# HG changeset patch
# User wenzelm
# Date 1364305124 -3600
# Node ID 637e64effda2fbd4f58b488fe62468dc0cab79f3
# Parent  abcd6d5f75081b3429d85ce240d8baa250a7e217
proper input event handling;

diff -r abcd6d5f7508 -r 637e64effda2 src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Tue Mar 26 14:14:39 2013 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Tue Mar 26 14:38:44 2013 +0100
@@ -11,7 +11,7 @@
 
 import scala.actors.Actor._
 import scala.swing.{FlowPanel, Label, ListView, Alignment, ScrollPane, Component, TextField}
-import scala.swing.event.{EditDone, MouseClicked}
+import scala.swing.event.{MouseClicked, ValueChanged}
 
 import java.lang.System
 import java.awt.{BorderLayout, Graphics2D, Insets, Color}
@@ -134,15 +134,16 @@
 
   private val threshold_value = new TextField(Time.print_seconds(timing_threshold)) {
     reactions += {
-      case EditDone(_) =>
+      case _: ValueChanged =>
         text match {
           case Properties.Value.Double(x) if x >= 0.0 => timing_threshold = x
           case _ =>
         }
-        text = Time.print_seconds(timing_threshold)
         handle_update()
     }
     tooltip = "Threshold for timing display (seconds)"
+    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)