clarified tooltip timing of pending event and active state;

--- a/src/Tools/jEdit/src/graphview_dockable.scala	Mon Jul 01 13:39:27 2013 +0200
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Mon Jul 01 14:30:56 2013 +0200
@@ -65,10 +65,13 @@
         new isabelle.graphview.Main_Panel(proper_graph) {
           override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
           {
-            val rendering = Rendering(snapshot, PIDE.options.value)
-            val screen_point = new Point(x, y)
-            SwingUtilities.convertPointToScreen(screen_point, parent)
-            Pretty_Tooltip(view, parent, rendering, screen_point, Command.Results.empty, body)
+            Pretty_Tooltip.invoke(() =>
+              {
+                val rendering = Rendering(snapshot, PIDE.options.value)
+                val screen_point = new Point(x, y)
+                SwingUtilities.convertPointToScreen(screen_point, parent)
+                Pretty_Tooltip(view, parent, rendering, screen_point, Command.Results.empty, body)
+              })
             null
           }
         }

--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Jul 01 13:39:27 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Jul 01 14:30:56 2013 +0200
@@ -60,29 +60,46 @@
   }
 
 
-  /* dismiss -- with global delay */
+  /* pending event and active state */  // owned by Swing thread
 
-  // owned by Swing thread
+  private var pending: Option[() => Unit] = None
   private var active = true
-  def is_active: Boolean = Swing_Thread.required { active }
+
+  private val pending_delay =
+    Swing_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) {
+      pending match {
+        case Some(body) => pending = None; body()
+        case None =>
+      }
+    }
 
-  // owned by Swing thread
+  def invoke(body: () => Unit): Unit =
+    Swing_Thread.required {
+      if (active) {
+        pending = Some(body)
+        pending_delay.invoke()
+      }
+    }
+
   private lazy val reactivate_delay =
     Swing_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) {
       active = true
     }
 
-  private def dismissing()
-  {
-    Swing_Thread.require()
+  private def deactivate(): Unit =
+    Swing_Thread.required {
+      pending = None
+      active = false
+      pending_delay.revoke()
+      reactivate_delay.invoke()
+    }
 
-    active = false
-    reactivate_delay.invoke()
-  }
+
+  /* dismiss */
 
   def dismiss(tip: Pretty_Tooltip)
   {
-    dismissing()
+    deactivate()
     hierarchy(tip) match {
       case Some((old, _ :: rest)) =>
         old.foreach(_.hide_popup)
@@ -94,7 +111,7 @@
 
   def dismiss_all()
   {
-    dismissing()
+    deactivate()
     stack.foreach(_.hide_popup)
     stack = Nil
   }

--- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Jul 01 13:39:27 2013 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Jul 01 14:30:56 2013 +0200
@@ -192,51 +192,38 @@
         }
         else active_reset()
 
-        if (Pretty_Tooltip.is_active) {
-          tooltip_event = Some(e)
-          tooltip_delay.invoke()
+        if (e.getSource == text_area.getPainter) {
+          Pretty_Tooltip.invoke(() =>
+            {
+              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 result =
+                      if (control) rendering.tooltip(range)
+                      else rendering.tooltip_message(range)
+                    result match {
+                      case None =>
+                      case Some(tip) =>
+                        val painter = text_area.getPainter
+                        val screen_point = e.getLocationOnScreen
+                        screen_point.translate(0, painter.getFontMetrics.getHeight / 2)
+                        val results = rendering.command_results(range)
+                        Pretty_Tooltip(view, painter, rendering, screen_point, results, tip.info)
+                    }
+                }
+              }
+            })
         }
       }
     }
   }
 
 
-  /* tooltips */
-
-  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 result =
-                  if (control) rendering.tooltip(range)
-                  else rendering.tooltip_message(range)
-                result match {
-                  case None =>
-                  case Some(tip) =>
-                    val painter = text_area.getPainter
-                    val screen_point = e.getLocationOnScreen
-                    screen_point.translate(0, painter.getFontMetrics.getHeight / 2)
-                    val results = rendering.command_results(range)
-                    Pretty_Tooltip(view, painter, rendering, screen_point, results, tip.info)
-                }
-            }
-          }
-          tooltip_event = None
-        case _ =>
-      }
-    }
-
-
   /* text background */
 
   private val background_painter = new TextAreaExtension