equal
deleted
inserted
replaced
94 private val update_button = new Button("Update") { |
94 private val update_button = new Button("Update") { |
95 tooltip = "Update display according to the command at cursor position" |
95 tooltip = "Update display according to the command at cursor position" |
96 reactions += { case ButtonClicked(_) => handle_update(true, None) } |
96 reactions += { case ButtonClicked(_) => handle_update(true, None) } |
97 } |
97 } |
98 |
98 |
99 private val zoom = new Font_Info.Zoom_Box { def changed() = handle_resize() } |
99 private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() } |
100 |
100 |
101 private val controls = |
101 private val controls = |
102 Wrap_Panel( |
102 Wrap_Panel( |
103 List(output_state_button, auto_update_button, |
103 List(output_state_button, auto_update_button, |
104 update_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom)) |
104 update_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom)) |