# HG changeset patch
# User wenzelm
# Date 1315144199 -7200
# Node ID 5199ee17c7d73895240611eea18fe4bde73a9619
# Parent  0385292321a0804a588e4e688a2b8433e812108d
property "tooltip-dismiss-delay" is edited in ms, not seconds;
explicit tooltip_dismiss_delay boundaries for further robustness;

diff -r 0385292321a0 -r 5199ee17c7d7 src/Pure/General/timing.scala
--- a/src/Pure/General/timing.scala	Sun Sep 04 15:21:50 2011 +0200
+++ b/src/Pure/General/timing.scala	Sun Sep 04 15:49:59 2011 +0200
@@ -9,6 +9,7 @@
 object Time
 {
   def seconds(s: Double): Time = new Time((s * 1000.0) round)
+  def ms(m: Long): Time = new Time(m)
 }
 
 class Time(val ms: Long)
diff -r 0385292321a0 -r 5199ee17c7d7 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])
   }
 }
diff -r 0385292321a0 -r 5199ee17c7d7 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sun Sep 04 15:21:50 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Sun Sep 04 15:49:59 2011 +0200
@@ -123,8 +123,10 @@
         Int_Property("tooltip-font-size", 10).toString + "px; \">" +  // FIXME proper scaling (!?)
       HTML.encode(text) + "</pre></html>"
 
+  private val tooltip_lb = Time.seconds(0.5)
+  private val tooltip_ub = Time.seconds(60.0)
   def tooltip_dismiss_delay(): Time =
-    Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max Time.seconds(0.5)
+    Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max tooltip_lb min tooltip_ub
 
   def setup_tooltips()
   {