src/Tools/jEdit/src/isabelle_options.scala

--- a/src/Tools/jEdit/src/isabelle_options.scala	Sun Sep 04 15:21:50 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Sun Sep 04 15:49:59 2011 +0200
@@ -63,6 +63,6 @@
       tooltip_margin.getValue().asInstanceOf[Int]
 
     Isabelle.Time_Property("tooltip-dismiss-delay") =
-      Time.seconds(tooltip_dismiss_delay.getValue().asInstanceOf[Int])
+      Time.ms(tooltip_dismiss_delay.getValue().asInstanceOf[Int])
   }
 }