# HG changeset patch
# User wenzelm
# Date 1283114856 -7200
# Node ID eb6a35be18ca13755167bbdb7d497c173b6d9de9
# Parent  f593754b07722a856c575449487330381d792fe7
Isabelle/jEdit property for global tooltip dismiss delay;

diff -r f593754b0772 -r eb6a35be18ca src/Tools/jEdit/plugin/Isabelle.props
--- a/src/Tools/jEdit/plugin/Isabelle.props	Sun Aug 29 21:21:37 2010 +0200
+++ b/src/Tools/jEdit/plugin/Isabelle.props	Sun Aug 29 22:47:36 2010 +0200
@@ -29,6 +29,8 @@
 options.isabelle.relative-font-size=100
 options.isabelle.tooltip-font-size.title=Tooltip Font Size
 options.isabelle.tooltip-font-size=10
+options.isabelle.tooltip-dismiss-delay.title=Tooltip Dismiss Delay (global)
+options.isabelle.tooltip-dismiss-delay=8000
 options.isabelle.startup-timeout=10000
 
 #menu actions
diff -r f593754b0772 -r eb6a35be18ca src/Tools/jEdit/src/jedit/isabelle_options.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_options.scala	Sun Aug 29 21:21:37 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala	Sun Aug 29 22:47:36 2010 +0200
@@ -17,6 +17,7 @@
   private val logic_name = new JComboBox()
   private val relative_font_size = new JSpinner()
   private val tooltip_font_size = new JSpinner()
+  private val tooltip_dismiss_delay = new JSpinner()
 
   private class List_Item(val name: String, val descr: String) {
     def this(name: String) = this(name, name)
@@ -46,6 +47,11 @@
       tooltip_font_size.setValue(Isabelle.Int_Property("tooltip-font-size", 10))
       tooltip_font_size
     })
+
+    addComponent(Isabelle.Property("tooltip-dismiss-delay.title"), {
+      tooltip_dismiss_delay.setValue(Isabelle.Int_Property("tooltip-dismiss-delay", 8000))
+      tooltip_dismiss_delay
+    })
   }
 
   override def _save()
@@ -58,5 +64,8 @@
 
     Isabelle.Int_Property("tooltip-font-size") =
       tooltip_font_size.getValue().asInstanceOf[Int]
+
+    Isabelle.Int_Property("tooltip-dismiss-delay") =
+      tooltip_dismiss_delay.getValue().asInstanceOf[Int]
   }
 }
diff -r f593754b0772 -r eb6a35be18ca src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Sun Aug 29 21:21:37 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Sun Aug 29 22:47:36 2010 +0200
@@ -81,6 +81,17 @@
         Int_Property("tooltip-font-size", 10).toString + "px; \">" +  // FIXME proper scaling (!?)
       HTML.encode(text) + "</pre></html>"
 
+  def tooltip_dismiss_delay(): Int =
+    Int_Property("tooltip-dismiss-delay", 8000) max 500
+
+  def setup_tooltips()
+  {
+    Swing_Thread.now {
+      val manager = javax.swing.ToolTipManager.sharedInstance
+      manager.setDismissDelay(tooltip_dismiss_delay())
+    }
+  }
+
 
   /* settings */
 
@@ -243,6 +254,8 @@
         Swing_Thread.now {
           for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined)
             Document_View(text_area).get.extend_styles()
+
+          Isabelle.setup_tooltips()
         }
 
         Isabelle.session.global_settings.event(Session.Global_Settings)
@@ -256,6 +269,8 @@
     Isabelle.system = new Isabelle_System
     Isabelle.system.install_fonts()
     Isabelle.session = new Session(Isabelle.system)  // FIXME dialog!?
+
+    Isabelle.setup_tooltips()
   }
 
   override def stop()