1    type Editor
2        def write (s : String) =
3            let endl @param = false
4            let color @param = TextColor.regular
5    
6            if should_separate then
7                should_separate = false
8                if not output.ends_with_two_blank_lines then
9                    output.append '\n'
10   
11           let line_index = output.lines.size - 1
12           output.append s
13           if endl then
14               output.append '\n'
15   
16           output.set_color line_index color
17           redraw
18   
19       def write_message (s : String) =
20           let color @param = TextColor.highlighted
21           write s =color
22                 endl = true
23   
24       def separate =
25           should_separate = true
26   
27       def clear_output =
28           should_separate = false
29           output.clear
30