# HG changeset patch
# User wenzelm
# Date 1349452908 -7200
# Node ID c91419b3a4256c43e9bd4d21791d799594e2b130
# Parent  519cf2ac6c0ead02e3fce772932422f1f3ac1f11
eliminated obsolete tooltip delay -- bypassed by Pretty_Tooltip;

diff -r 519cf2ac6c0e -r c91419b3a425 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Fri Oct 05 14:51:33 2012 +0200
+++ b/src/Tools/jEdit/etc/options	Fri Oct 05 18:01:48 2012 +0200
@@ -15,9 +15,6 @@
 option jedit_tooltip_margin : int = 60
   -- "margin for tooltip pretty-printing"
 
-option jedit_tooltip_dismiss_delay : real = 8.0
-  -- "global delay for Swing tooltips"
-
 option jedit_text_overview : bool = true
   -- "paint text overview column (potentially slow for large files)"
 
diff -r 519cf2ac6c0e -r c91419b3a425 src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala	Fri Oct 05 14:51:33 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Fri Oct 05 18:01:48 2012 +0200
@@ -42,9 +42,8 @@
   // FIXME avoid hard-wired stuff
   private val relevant_options =
     Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_text_overview",
-      "jedit_tooltip_font_scale", "jedit_tooltip_margin", "jedit_tooltip_dismiss_delay",
-      "editor_load_delay", "editor_input_delay", "editor_output_delay",
-      "editor_update_delay", "editor_reparse_limit")
+      "jedit_tooltip_font_scale", "jedit_tooltip_margin", "editor_load_delay",
+      "editor_input_delay", "editor_output_delay", "editor_update_delay", "editor_reparse_limit")
 
   relevant_options.foreach(Isabelle.options.value.check_name _)
 
diff -r 519cf2ac6c0e -r c91419b3a425 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Fri Oct 05 14:51:33 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Oct 05 18:01:48 2012 +0200
@@ -55,22 +55,6 @@
     (jEdit.getIntegerProperty("view.fontsize", 16) * options.real(scale)).toFloat
 
 
-  /* tooltip delay */
-
-  private val tooltip_lb = Time.seconds(0.5)
-  private val tooltip_ub = Time.seconds(60.0)
-  def tooltip_dismiss_delay(): Time =
-    Time.seconds(options.real("jedit_tooltip_dismiss_delay")) max tooltip_lb min tooltip_ub
-
-  def setup_tooltips()
-  {
-    Swing_Thread.now {
-      val manager = javax.swing.ToolTipManager.sharedInstance
-      manager.setDismissDelay(tooltip_dismiss_delay().ms.toInt)
-    }
-  }
-
-
   /* document model and view */
 
   def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
@@ -312,7 +296,6 @@
           }
 
         case msg: PropertiesChanged =>
-          Isabelle.setup_tooltips()
           Isabelle.session.global_options.event(Session.Global_Options)
 
         case _ =>
@@ -328,10 +311,7 @@
       Isabelle_System.install_fonts()
 
       val init_options = Options.init()
-      Swing_Thread.now {
-        Isabelle.options.update(init_options)
-        Isabelle.setup_tooltips()
-      }
+      Swing_Thread.now { Isabelle.options.update(init_options)  }
 
       SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
       if (ModeProvider.instance.isInstanceOf[ModeProvider])