--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Wed Jun 09 18:24:23 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Fri Jun 11 21:58:40 2010 +0200
@@ -129,19 +129,18 @@
reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() }
}
tracing.selected = show_tracing
- tracing.tooltip =
- "<html>Indicate output of tracing messages<br>(also needs to be enabled on the prover side)</html>"
+ tracing.tooltip = "Indicate output of tracing messages"
private val auto_update = new CheckBox("Auto update") {
reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() }
}
auto_update.selected = follow_caret
- auto_update.tooltip = "<html>Indicate automatic update following cursor movement</html>"
+ auto_update.tooltip = "Indicate automatic update following cursor movement"
private val update = new Button("Update") {
reactions += { case ButtonClicked(_) => handle_caret(); handle_update() }
}
- update.tooltip = "<html>Update display according to the command at cursor position</html>"
+ update.tooltip = "Update display according to the command at cursor position"
val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, debug, tracing, auto_update, update)
add(controls.peer, BorderLayout.NORTH)