diff -r 8662b9b1f123 -r 09270033330e src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Wed Dec 01 20:34:40 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Wed Dec 01 21:07:50 2010 +0100
@@ -111,14 +111,14 @@
         Int_Property("tooltip-font-size", 10).toString + "px; \">" +  // FIXME proper scaling (!?)
       HTML.encode(text) + "</pre></html>"
 
-  def tooltip_dismiss_delay(): Int =
-    Int_Property("tooltip-dismiss-delay", 8000) max 500
+  def tooltip_dismiss_delay(): Time =
+    Time.seconds(Double_Property("tooltip-dismiss-delay", 8.0) max 0.5)
 
   def setup_tooltips()
   {
     Swing_Thread.now {
       val manager = javax.swing.ToolTipManager.sharedInstance
-      manager.setDismissDelay(tooltip_dismiss_delay())
+      manager.setDismissDelay(tooltip_dismiss_delay().ms.toInt)
     }
   }