1     def load_text (text_box : MultilineTextBox) (s : String) =
2         let text = text_box.display_text
3         if text.is_not_empty then
4             text.clear
5     
6         text.insert TextPos.new s
7         text_box.update_colors 0 text.lines.size
8                  update_visuals
9     
10    type Editor
11        val tree = Tree
12            =data
13            min_width = 320
14    
15        val output_text_box = MultilineTextBox
16            min_width = 320
17            is_readonly = true
18    
19        local output = output_text_box.display_text
20    
21        val tab_control = TabControl
22            set_foreground = false
23            on_closing = { args ->
24                let text_box = tab_item_text_boxes[args.tab_item]
25                if text_box.is_changed && not app.os_window.is_control_pressed then
26                    args.is_cancelled = true }
27    
28            on_closed = { tab_item ->
29                let file_item = tab_item_file_items[tab_item]
30                tab_item_text_boxes.remove tab_item
31                tab_item_file_items.remove tab_item
32                file_item_tab_items.remove file_item }
33    
34        val apply_button = Button.new
35        val revert_margin = Margin.new
36        let menu = Menu
37            apply_button
38                text = "apply"
39                command = Command/Apply
40                is_visible = false
41            revert_margin
42                is_visible = false
43                right = 40
44                Button
45                    text = "revert"
46                    command = Command/Revert
47            MenuItem
48                text = "file"
49                Button
50                    text = "new"
51                    command = Command/File
52                Button
53                    text = "directory"
54                    command = Command/Directory
55                Button
56                    text = "save all"
57                    command = Command/SaveAll
58            MenuItem
59                text = "edit"
60                Button
61                    text = "rename"
62                    command = Command/Rename
63                Button
64                    text = "delete"
65                    command = Command/Delete
66    
67        let left_border = Border
68            right = 1
69            color = control/Colors.shade3
70            Rectangle
71                color = Colors.tree_background
72                Scroller
73                    tree
74    
75        let right_border = Border
76            left = 1
77            color = control/Colors.shade3
78            output_text_box
79    
80        let rectangle = Rectangle
81            color = Colors.background
82            Resizer
83                Resizer
84                    is_first_primary = false
85                    separator_offset = 1
86                    left_border
87                    tab_control
88    
89                right_border
90    
91        let splitter = Splitter
92            ratio = 0
93            is_vertical = true
94            Border
95                down = 1
96                color = control/Colors.shade3
97                menu
98            rectangle
99    
100       app.set_content splitter
101   
102       tab_control.selected_tab_item@atom.subscribe
103           { maybe_prev_tab_item maybe_tab_item ->
104                 if maybe_prev_tab_item.is_some && maybe_tab_item.is_some then
105                     let prev_tab_item = maybe_prev_tab_item.unwrap
106                     let tab_item = maybe_tab_item.unwrap
107                     let prev_text_box = tab_item_text_boxes[prev_tab_item]
108                     if app.display.focus == Some prev_text_box then
109                         let text_box = tab_item_text_boxes[tab_item]
110                         app.display.focus = text_box }
111       |> tokens.add
112   
113       let default_foreground = apply_button.foreground
114       changed.bind
115           { index _ -> if index == 0 && changed.size == 1 then
116                            apply_button.is_visible = true
117                            revert_margin.is_visible = true }
118   
119           { index _ -> if index == 0 && changed.is_empty then
120                            apply_button.is_visible = false
121                            revert_margin.is_visible = false }
122       |> tokens.add
123