src/Tools/jEdit/src/plugin.scala
changeset 44699 5199ee17c7d7
parent 44615 a4ff8a787202
child 44721 ba478c3f7255
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Sun Sep 04 15:21:50 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sun Sep 04 15:49:59 2011 +0200
     1.3 @@ -123,8 +123,10 @@
     1.4          Int_Property("tooltip-font-size", 10).toString + "px; \">" +  // FIXME proper scaling (!?)
     1.5        HTML.encode(text) + "</pre></html>"
     1.6  
     1.7 +  private val tooltip_lb = Time.seconds(0.5)
     1.8 +  private val tooltip_ub = Time.seconds(60.0)
     1.9    def tooltip_dismiss_delay(): Time =
    1.10 -    Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max Time.seconds(0.5)
    1.11 +    Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max tooltip_lb min tooltip_ub
    1.12  
    1.13    def setup_tooltips()
    1.14    {