# HG changeset patch
# User wenzelm
# Date 1375730586 -7200
# Node ID 8d8cb75ab20a9f5a717da35c9ebf8f279d60d883
# Parent  438f578ef1d9b28eff83d1c0ff0bce14702db830
more central Pretty_Tooltip.dismissed_all -- avoid spurious crash of Rich_Text_Area.robust_body in asynchronous mouse_motion_listener;

diff -r 438f578ef1d9 -r 8d8cb75ab20a src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Aug 05 17:52:07 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Aug 05 21:23:06 2013 +0200
@@ -272,7 +272,10 @@
               if (PIDE.session.is_ready)
                 PIDE.init_view(buffer, text_area)
             }
-            else PIDE.exit_view(buffer, text_area)
+            else {
+              Pretty_Tooltip.dismissed_all()
+              PIDE.exit_view(buffer, text_area)
+            }
           }
 
         case msg: PropertiesChanged =>
diff -r 438f578ef1d9 -r 8d8cb75ab20a src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Aug 05 17:52:07 2013 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Aug 05 21:23:06 2013 +0200
@@ -156,7 +156,6 @@
       robust_body(()) {
         hyperlink_area.info match {
           case Some(Text.Info(_, link)) =>
-            Pretty_Tooltip.dismissed_all()
             link.follow(view)
           case None =>
         }