more central Pretty_Tooltip.dismissed_all -- avoid spurious crash of Rich_Text_Area.robust_body in asynchronous mouse_motion_listener;

--- 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 =>

--- 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 =>
         }