1 type Editor 2 def open (item : FileItem) : bool = 3 if item.is_directory then 4 return false 5 6 if file_item_tab_items.contains item then 7 let tab_item = file_item_tab_items[item] 8 tab_control.select tab_item 9 false 10 else 11 let name = item.name 12 let file_text = if item.actual_path.is_empty 13 then "" 14 else fs/read_text item.actual_path 15 16 let text_box = MultilineTextBox 17 min_width = 400 18 text = file_text 19 show_line_numbers = true 20 update_colors = { update_colors _ _ _ } 21 22 load_text text_box file_text 23 24 let margin = Margin 25 up = 10 26 content = text_box 27 28 control/arrange_unmeasured margin 29 tab_control.presenter.width 30 tab_control.presenter.height 31 32 let tab_item = TabItem 33 header = name 34 can_close = true 35 margin 36 37 text_box.is_changed@atom.subscribe 38 { _ x -> let color = if x 39 then Colors.blue 40 else tab_control.foreground 41 42 item.foreground = color 43 if x then content_changed.add item 44 else content_changed.remove item } 45 |> tab_item.push_token 46 47 item.foreground@atom.bind { tab_item.foreground = _ } 48 |> tab_item.push_token 49 50 tab_item_text_boxes.add tab_item text_box 51 file_item_tab_items.add item tab_item 52 tab_item_file_items.add tab_item item 53 tab_control.tab_items.add tab_item 54 select tab_item 55 true 56 57 tree.on_open.add { item -> 58 let file = item as FileItem 59 if file.is_directory then 60 file.is_open = not file.is_open 61 else 62 open file |> ignore } 63