# HG changeset patch
# User wenzelm
# Date 1291234070 -3600
# Node ID 09270033330e9c27367dba98a683f30d13c366c5
# Parent  8662b9b1f1232716187d15daf0baa8def071c15e
store tooltip-dismiss-delay as Double(seconds);

diff -r 8662b9b1f123 -r 09270033330e src/Tools/jEdit/plugin/Isabelle.props
--- a/src/Tools/jEdit/plugin/Isabelle.props	Wed Dec 01 20:34:40 2010 +0100
+++ b/src/Tools/jEdit/plugin/Isabelle.props	Wed Dec 01 21:07:50 2010 +0100
@@ -32,7 +32,7 @@
 options.isabelle.tooltip-margin.title=Tooltip Margin
 options.isabelle.tooltip-margin=40
 options.isabelle.tooltip-dismiss-delay.title=Tooltip Dismiss Delay (global)
-options.isabelle.tooltip-dismiss-delay=8000
+options.isabelle.tooltip-dismiss-delay=8.0
 options.isabelle.startup-timeout=10.0
 options.isabelle.auto-start.title=Auto Start
 options.isabelle.auto-start=true
diff -r 8662b9b1f123 -r 09270033330e src/Tools/jEdit/src/jedit/isabelle_options.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_options.scala	Wed Dec 01 20:34:40 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala	Wed Dec 01 21:07:50 2010 +0100
@@ -39,7 +39,8 @@
     tooltip_margin.setValue(Isabelle.Int_Property("tooltip-margin", 40))
     addComponent(Isabelle.Property("tooltip-margin.title"), tooltip_margin)
 
-    tooltip_dismiss_delay.setValue(Isabelle.Int_Property("tooltip-dismiss-delay", 8000))
+    tooltip_dismiss_delay.setValue(
+      (Isabelle.Double_Property("tooltip-dismiss-delay", 8.0) * 1000) round)
     addComponent(Isabelle.Property("tooltip-dismiss-delay.title"), tooltip_dismiss_delay)
   }
 
@@ -58,7 +59,7 @@
     Isabelle.Int_Property("tooltip-margin") =
       tooltip_margin.getValue().asInstanceOf[Int]
 
-    Isabelle.Int_Property("tooltip-dismiss-delay") =
-      tooltip_dismiss_delay.getValue().asInstanceOf[Int]
+    Isabelle.Double_Property("tooltip-dismiss-delay") =
+      tooltip_dismiss_delay.getValue().asInstanceOf[Int].toDouble / 1000
   }
 }
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)
     }
   }