1 local text_position_to_y (text_display : TextDisplay) (position : TextPos) = 2 let up = position.line * text_display.font.line_height 3 let down = up + text_display.font.line_height + text_display.margin.up 4 (up, down) 5 6 type MultilineTextBox 7 let selection_color = Colors.multiline_text_box_selection 8 local (selection_start, selection_middle, selection_end) = 9 let args = (color = selection_color 10 is_visible = false) 11 12 (Rectangle f@ args 13 Rectangle f@ args 14 Rectangle f@ args) 15 16 val text_display = TextDisplay font 17 margin = text_margin 18 offset_y = selection_offset_y 19 val numbers_display = TextDisplay font 20 margin = text_margin 21 val scroller = Scroller.new 22 let numbers_border = Border.new 23 local scissor_control = ScissorControl.new 24 25 local canvas = Canvas 26 exclude_width <- selection_start 27 selection_middle 28 selection_end 29 text_display 30 31 show_line_numbers@atom.bind { numbers_border.is_visible = _ } 32 |> push_token 33 34 let rectangle = Rectangle 35 color@obs = background@obs 36 scroller 37 Splitter 38 ratio = 0 39 numbers_border 40 right = 1 41 color = Colors.multiline_text_box_numbers_border 42 Rectangle 43 color = Colors.multiline_text_box_numbers_background 44 Margin 45 right = 24 46 numbers_display 47 scissor_control 48 canvas 49 selection_start 50 selection_middle 51 selection_end 52 text_display 53 54 content = rectangle 55 offset_controls.add text_display 56 add selection_start 57 add selection_middle 58 add selection_end 59 60 def update_colors (from : u32) (to : u32) = 61 if update_colors ? Some f then 62 f display_text from to 63 64 def update_colors (index : u32) = 65 update_colors index index 66 67 def show self (position : TextPos) = 68 let scroller = self.scroller 69 70 let scroll_to (y : u32) = 71 scroller/move_to scroller None -y.as<i32> 72 73 let font = self.font 74 let (up, down) = text_position_to_y self.text_display position 75 if scroller.visible_y.down - font.line_height < down then 76 let y = down + font.line_height 77 + scroller.visible_y.up - scroller.visible_y.down 78 79 scroll_to y 80 81 else if scroller.visible_y.up + font.line_height > up then 82 let y = if up > font.line_height 83 then up - font.line_height 84 else 0 85 86 scroll_to y 87