# HG changeset patch # User wenzelm # Date 1276286320 -7200 # Node ID babe498016e8a8360dcbaf15846d81d8eee7decc # Parent dced658407c41b6a112234eb03837eb59ea16446 tuned tooltips; diff -r dced658407c4 -r babe498016e8 src/Tools/jEdit/src/jedit/output_dockable.scala --- 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 = - "Indicate output of tracing messages
(also needs to be enabled on the prover side)" + 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 = "Indicate automatic update following cursor movement" + auto_update.tooltip = "Indicate automatic update following cursor movement" private val update = new Button("Update") { reactions += { case ButtonClicked(_) => handle_caret(); handle_update() } } - update.tooltip = "Update display according to the command at cursor position" + 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)