1 let number_lines = 2 let lines = List<TextLine>.new 3 for i = 1 to 10000 do 4 let line = TextLine.new 5 line.insert 0 "$i\n" 6 line.set_color light_gray 7 lines.add line 8 9 lines 10 11 type MultilineTextBox 12 text_display.set_z Control.offset_z 13 numbers_display.set_z Control.offset_z 14 15 def update_mesh self = 16 let (visible_up, visible_down) = self.scroller.visible_y 17 self.text_display.text = self.display_text.lines.as_slice 18 visible_up = visible_up 19 visible_down = visible_down 20 selection = self.selection 21 update 22 23 if self.show_line_numbers then 24 val numbers_selection = Some (TextPos.new, TextPos.max) 25 self.numbers_display.text = 26 number_lines.as_slice.take self.display_text.lines.size 27 28 self.numbers_display.visible_up = visible_up 29 visible_down = visible_down 30 selection = numbers_selection 31 update 32 else 33 self.numbers_display.set_fixed_width 0 34 set_fixed_height 0 35 36 def update = 37 update_mesh 38 update_offset 39 40 scroller.visible_y@atom.subscribe { update_mesh } |> push_token 41 42 endmodule multiline_text_box 43 44 import multiline_text_box/MultilineTextBox 45