explicit Pretty_Tooltip.dismiss_all due to slightly changed focus mechanics;

--- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Jun 29 20:25:33 2013 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Jun 29 20:40:08 2013 +0200
@@ -155,7 +155,9 @@
     override def mouseClicked(e: MouseEvent) {
       robust_body(()) {
         hyperlink_area.info match {
-          case Some(Text.Info(_, link)) => link.follow(view)
+          case Some(Text.Info(_, link)) =>
+            Pretty_Tooltip.dismiss_all()
+            link.follow(view)
           case None =>
         }
         active_area.text_info match {