src/Tools/jEdit/src/timing_dockable.scala

 
   /* timing threshold */
 
   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 += {
       case _: ValueChanged =>
         text match {
           case Properties.Value.Double(x) if x >= 0.0 => timing_threshold = x
           case _ =>
         }
         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 })
   }
 
   private val controls = new FlowPanel(FlowPanel.Alignment.Right)(threshold_label, threshold_value)