equal
deleted
inserted
replaced
138 private val update = new Button("Update") { |
138 private val update = new Button("Update") { |
139 tooltip = "Update display according to the command at cursor position" |
139 tooltip = "Update display according to the command at cursor position" |
140 reactions += { case ButtonClicked(_) => handle_update(true, None) } |
140 reactions += { case ButtonClicked(_) => handle_update(true, None) } |
141 } |
141 } |
142 |
142 |
143 private val detach = new Button("Detach") { |
143 private val detach = pretty_text_area.make_detach_button |
144 tooltip = "Detach window with static copy of current output" |
|
145 reactions += { case ButtonClicked(_) => pretty_text_area.detach } |
|
146 } |
|
147 |
144 |
148 private val controls = |
145 private val controls = |
149 new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update, update, detach, zoom) |
146 new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update, update, detach, zoom) |
150 add(controls.peer, BorderLayout.NORTH) |
147 add(controls.peer, BorderLayout.NORTH) |
151 } |
148 } |