# HG changeset patch
# User wenzelm
# Date 1364381693 -3600
# Node ID 37211c7c2894a31ad6f471401933c0dfa76b69ca
# Parent  6f6012f430fca7715294e84aac015d522cf4d2ae
tuned GUI;

diff -r 6f6012f430fc -r 37211c7c2894 src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Tue Mar 26 20:55:21 2013 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Wed Mar 27 11:54:53 2013 +0100
@@ -130,7 +130,11 @@
 
   private var timing_threshold = PIDE.options.real("jedit_timing_threshold")
 
-  private val threshold_label = new Label("Threshold: ")
+  private val threshold_tooltip = "Threshold for timing display (seconds)"
+
+  private val threshold_label = new Label("Threshold: ") {
+    tooltip = threshold_tooltip
+  }
 
   private val threshold_value = new TextField(Time.print_seconds(timing_threshold)) {
     reactions += {
@@ -141,7 +145,7 @@
         }
         handle_update()
     }
-    tooltip = "Threshold for timing display (seconds)"
+    tooltip = threshold_tooltip
     verifier = ((s: String) =>
       s match { case Properties.Value.Double(x) => x >= 0.0 case _ => false })
   }