--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Fri May 21 11:51:03 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Fri May 21 12:59:44 2010 +0200
@@ -63,12 +63,15 @@
}
private val zoom = Library.zoom_box(factor => { zoom_factor = factor; handle_resize() })
+ zoom.tooltip = "Zoom factor for basic font size"
private val update = new Button("Update") {
reactions += { case ButtonClicked(_) => handle_update() }
}
+ update.tooltip = "Update display according to state of command at caret position"
private val follow = new CheckBox("Follow")
+ follow.tooltip = "Indicate automatic update according to caret movement or state changes"
follow.selected = true