Isabelle/jEdit property for global tooltip dismiss delay;
authorwenzelm
Sun Aug 29 22:47:36 2010 +0200 (2010-08-29)
changeset 38854eb6a35be18ca
parent 38853 f593754b0772
child 38855 35b2d91e88d7
Isabelle/jEdit property for global tooltip dismiss delay;
src/Tools/jEdit/plugin/Isabelle.props
src/Tools/jEdit/src/jedit/isabelle_options.scala
src/Tools/jEdit/src/jedit/plugin.scala
     1.1 --- a/src/Tools/jEdit/plugin/Isabelle.props	Sun Aug 29 21:21:37 2010 +0200
     1.2 +++ b/src/Tools/jEdit/plugin/Isabelle.props	Sun Aug 29 22:47:36 2010 +0200
     1.3 @@ -29,6 +29,8 @@
     1.4  options.isabelle.relative-font-size=100
     1.5  options.isabelle.tooltip-font-size.title=Tooltip Font Size
     1.6  options.isabelle.tooltip-font-size=10
     1.7 +options.isabelle.tooltip-dismiss-delay.title=Tooltip Dismiss Delay (global)
     1.8 +options.isabelle.tooltip-dismiss-delay=8000
     1.9  options.isabelle.startup-timeout=10000
    1.10  
    1.11  #menu actions
     2.1 --- a/src/Tools/jEdit/src/jedit/isabelle_options.scala	Sun Aug 29 21:21:37 2010 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala	Sun Aug 29 22:47:36 2010 +0200
     2.3 @@ -17,6 +17,7 @@
     2.4    private val logic_name = new JComboBox()
     2.5    private val relative_font_size = new JSpinner()
     2.6    private val tooltip_font_size = new JSpinner()
     2.7 +  private val tooltip_dismiss_delay = new JSpinner()
     2.8  
     2.9    private class List_Item(val name: String, val descr: String) {
    2.10      def this(name: String) = this(name, name)
    2.11 @@ -46,6 +47,11 @@
    2.12        tooltip_font_size.setValue(Isabelle.Int_Property("tooltip-font-size", 10))
    2.13        tooltip_font_size
    2.14      })
    2.15 +
    2.16 +    addComponent(Isabelle.Property("tooltip-dismiss-delay.title"), {
    2.17 +      tooltip_dismiss_delay.setValue(Isabelle.Int_Property("tooltip-dismiss-delay", 8000))
    2.18 +      tooltip_dismiss_delay
    2.19 +    })
    2.20    }
    2.21  
    2.22    override def _save()
    2.23 @@ -58,5 +64,8 @@
    2.24  
    2.25      Isabelle.Int_Property("tooltip-font-size") =
    2.26        tooltip_font_size.getValue().asInstanceOf[Int]
    2.27 +
    2.28 +    Isabelle.Int_Property("tooltip-dismiss-delay") =
    2.29 +      tooltip_dismiss_delay.getValue().asInstanceOf[Int]
    2.30    }
    2.31  }
     3.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Sun Aug 29 21:21:37 2010 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Sun Aug 29 22:47:36 2010 +0200
     3.3 @@ -81,6 +81,17 @@
     3.4          Int_Property("tooltip-font-size", 10).toString + "px; \">" +  // FIXME proper scaling (!?)
     3.5        HTML.encode(text) + "</pre></html>"
     3.6  
     3.7 +  def tooltip_dismiss_delay(): Int =
     3.8 +    Int_Property("tooltip-dismiss-delay", 8000) max 500
     3.9 +
    3.10 +  def setup_tooltips()
    3.11 +  {
    3.12 +    Swing_Thread.now {
    3.13 +      val manager = javax.swing.ToolTipManager.sharedInstance
    3.14 +      manager.setDismissDelay(tooltip_dismiss_delay())
    3.15 +    }
    3.16 +  }
    3.17 +
    3.18  
    3.19    /* settings */
    3.20  
    3.21 @@ -243,6 +254,8 @@
    3.22          Swing_Thread.now {
    3.23            for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined)
    3.24              Document_View(text_area).get.extend_styles()
    3.25 +
    3.26 +          Isabelle.setup_tooltips()
    3.27          }
    3.28  
    3.29          Isabelle.session.global_settings.event(Session.Global_Settings)
    3.30 @@ -256,6 +269,8 @@
    3.31      Isabelle.system = new Isabelle_System
    3.32      Isabelle.system.install_fonts()
    3.33      Isabelle.session = new Session(Isabelle.system)  // FIXME dialog!?
    3.34 +
    3.35 +    Isabelle.setup_tooltips()
    3.36    }
    3.37  
    3.38    override def stop()