127 |
127 |
128 private val tracing = new CheckBox("Tracing") { |
128 private val tracing = new CheckBox("Tracing") { |
129 reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() } |
129 reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() } |
130 } |
130 } |
131 tracing.selected = show_tracing |
131 tracing.selected = show_tracing |
132 tracing.tooltip = |
132 tracing.tooltip = "Indicate output of tracing messages" |
133 "<html>Indicate output of tracing messages<br>(also needs to be enabled on the prover side)</html>" |
|
134 |
133 |
135 private val auto_update = new CheckBox("Auto update") { |
134 private val auto_update = new CheckBox("Auto update") { |
136 reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() } |
135 reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() } |
137 } |
136 } |
138 auto_update.selected = follow_caret |
137 auto_update.selected = follow_caret |
139 auto_update.tooltip = "<html>Indicate automatic update following cursor movement</html>" |
138 auto_update.tooltip = "Indicate automatic update following cursor movement" |
140 |
139 |
141 private val update = new Button("Update") { |
140 private val update = new Button("Update") { |
142 reactions += { case ButtonClicked(_) => handle_caret(); handle_update() } |
141 reactions += { case ButtonClicked(_) => handle_caret(); handle_update() } |
143 } |
142 } |
144 update.tooltip = "<html>Update display according to the command at cursor position</html>" |
143 update.tooltip = "Update display according to the command at cursor position" |
145 |
144 |
146 val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, debug, tracing, auto_update, update) |
145 val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, debug, tracing, auto_update, update) |
147 add(controls.peer, BorderLayout.NORTH) |
146 add(controls.peer, BorderLayout.NORTH) |
148 |
147 |
149 handle_update() |
148 handle_update() |