added some tooltips;
authorwenzelm
Fri, 21 May 2010 12:59:44 +0200
changeset 37037 35d45feccbc6
parent 37036 49559c4e85f9
child 37038 1ce1b19f78f4
added some tooltips;
src/Tools/jEdit/src/jedit/output_dockable.scala
--- 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