src/Tools/jEdit/src/plugin.scala
changeset 44699 5199ee17c7d7
parent 44615 a4ff8a787202
child 44721 ba478c3f7255
--- 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()
   {