property "tooltip-dismiss-delay" is edited in ms, not seconds;
authorwenzelm
Sun Sep 04 15:49:59 2011 +0200 (2011-09-04)
changeset 446995199ee17c7d7
parent 44698 0385292321a0
child 44700 f4b42f310f86
property "tooltip-dismiss-delay" is edited in ms, not seconds;
explicit tooltip_dismiss_delay boundaries for further robustness;
src/Pure/General/timing.scala
src/Tools/jEdit/src/isabelle_options.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/General/timing.scala	Sun Sep 04 15:21:50 2011 +0200
     1.2 +++ b/src/Pure/General/timing.scala	Sun Sep 04 15:49:59 2011 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  object Time
     1.5  {
     1.6    def seconds(s: Double): Time = new Time((s * 1000.0) round)
     1.7 +  def ms(m: Long): Time = new Time(m)
     1.8  }
     1.9  
    1.10  class Time(val ms: Long)
     2.1 --- a/src/Tools/jEdit/src/isabelle_options.scala	Sun Sep 04 15:21:50 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/isabelle_options.scala	Sun Sep 04 15:49:59 2011 +0200
     2.3 @@ -63,6 +63,6 @@
     2.4        tooltip_margin.getValue().asInstanceOf[Int]
     2.5  
     2.6      Isabelle.Time_Property("tooltip-dismiss-delay") =
     2.7 -      Time.seconds(tooltip_dismiss_delay.getValue().asInstanceOf[Int])
     2.8 +      Time.ms(tooltip_dismiss_delay.getValue().asInstanceOf[Int])
     2.9    }
    2.10  }
     3.1 --- a/src/Tools/jEdit/src/plugin.scala	Sun Sep 04 15:21:50 2011 +0200
     3.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sun Sep 04 15:49:59 2011 +0200
     3.3 @@ -123,8 +123,10 @@
     3.4          Int_Property("tooltip-font-size", 10).toString + "px; \">" +  // FIXME proper scaling (!?)
     3.5        HTML.encode(text) + "</pre></html>"
     3.6  
     3.7 +  private val tooltip_lb = Time.seconds(0.5)
     3.8 +  private val tooltip_ub = Time.seconds(60.0)
     3.9    def tooltip_dismiss_delay(): Time =
    3.10 -    Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max Time.seconds(0.5)
    3.11 +    Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max tooltip_lb min tooltip_ub
    3.12  
    3.13    def setup_tooltips()
    3.14    {