more elementary tooltips via mouse events (imitating parts of javax.swing.ToolTipManager) -- avoid abuse of getToolTipText to produce window as side-effect;

--- a/src/Tools/jEdit/etc/options	Sat Mar 16 17:16:39 2013 +0100
+++ b/src/Tools/jEdit/etc/options	Sat Mar 16 21:26:44 2013 +0100
@@ -6,6 +6,9 @@
 option jedit_font_scale : real = 1.0
   -- "scale factor of add-on panels wrt. main text area"
 
+option jedit_tooltip_delay : real = 0.75
+  -- "delay for semantic tooltip popup"
+
 option jedit_tooltip_font_scale : real = 0.85
   -- "scale factor of tooltips wrt. main text area"
 

--- a/src/Tools/jEdit/src/isabelle_options.scala	Sat Mar 16 17:16:39 2013 +0100
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Sat Mar 16 21:26:44 2013 +0100
@@ -42,11 +42,11 @@
   // FIXME avoid hard-wired stuff
   private val relevant_options =
     Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit",
-      "jedit_text_overview_limit", "jedit_tooltip_bounds", "jedit_tooltip_font_scale",
-      "jedit_tooltip_margin", "jedit_mac_adapter", "threads", "threads_trace", "parallel_proofs",
-      "parallel_subproofs_saturation", "editor_load_delay", "editor_input_delay",
-      "editor_output_delay", "editor_reparse_limit", "editor_tracing_messages",
-      "editor_update_delay", "editor_chart_delay")
+      "jedit_text_overview_limit", "jedit_tooltip_bounds", "jedit_tooltip_delay",
+      "jedit_tooltip_font_scale", "jedit_tooltip_margin", "jedit_mac_adapter", "threads",
+      "threads_trace", "parallel_proofs", "parallel_subproofs_saturation", "editor_load_delay",
+      "editor_input_delay", "editor_output_delay", "editor_reparse_limit",
+      "editor_tracing_messages", "editor_update_delay", "editor_chart_delay")
 
   relevant_options.foreach(PIDE.options.value.check_name _)
 

--- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Mar 16 17:16:39 2013 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Mar 16 21:26:44 2013 +0100
@@ -175,7 +175,7 @@
 
         if ((control || hovering) && !buffer.isLoading) {
           JEdit_Lib.buffer_lock(buffer) {
-            JEdit_Lib.pixel_range(text_area, e.getX(), e.getY()) match {
+            JEdit_Lib.pixel_range(text_area, e.getX, e.getY) match {
               case None => active_reset()
               case Some(range) =>
                 val rendering = get_rendering()
@@ -189,6 +189,9 @@
           }
         }
         else active_reset()
+
+        tooltip_event = Some(e)
+        tooltip_delay.invoke()
       }
     }
   }
@@ -196,32 +199,35 @@
 
   /* tooltips */
 
-  private val tooltip_painter = new TextAreaExtension
-  {
-    override def getToolTipText(x: Int, y: Int): String =
-    {
-      robust_body(null: String) {
-        val rendering = get_rendering()
-        val snapshot = rendering.snapshot
-        if (!snapshot.is_outdated) {
-          JEdit_Lib.pixel_range(text_area, x, y) match {
-            case None =>
-            case Some(range) =>
-              val tip =
-                if (control) rendering.tooltip(range)
-                else rendering.tooltip_message(range)
-              if (!tip.isEmpty) {
-                val painter = text_area.getPainter
-                val y1 = y + painter.getFontMetrics.getHeight / 2
-                val results = rendering.command_results(range)
-                new Pretty_Tooltip(view, painter, rendering, x, y1, results, tip)
-              }
+  private var tooltip_event: Option[MouseEvent] = None
+
+  private val tooltip_delay =
+    Swing_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) {
+      tooltip_event match {
+        case Some(e) if e.getSource == text_area.getPainter =>
+          val rendering = get_rendering()
+          val snapshot = rendering.snapshot
+          if (!snapshot.is_outdated) {
+            val x = e.getX
+            val y = e.getY
+            JEdit_Lib.pixel_range(text_area, x, y) match {
+              case None =>
+              case Some(range) =>
+                val tip =
+                  if (control) rendering.tooltip(range)
+                  else rendering.tooltip_message(range)
+                if (!tip.isEmpty) {
+                  val painter = text_area.getPainter
+                  val y1 = y + painter.getFontMetrics.getHeight / 2
+                  val results = rendering.command_results(range)
+                  new Pretty_Tooltip(view, painter, rendering, x, y1, results, tip)
+                }
+            }
           }
-        }
-        null
+          tooltip_event = None
+        case _ =>
       }
     }
-  }
 
 
   /* text background */
@@ -507,7 +513,6 @@
   {
     val painter = text_area.getPainter
     painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state)
-    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, tooltip_painter)
     painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
     painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
     painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1)
@@ -541,7 +546,6 @@
     painter.removeExtension(before_caret_painter1)
     painter.removeExtension(text_painter)
     painter.removeExtension(background_painter)
-    painter.removeExtension(tooltip_painter)
     painter.removeExtension(set_state)
   }
 }