--- 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 })
}