# HG changeset patch
# User wenzelm
# Date 1372531208 -7200
# Node ID 5b7c4fb41511073faf94a608df12ac5b76c52c73
# Parent  d977e7eb7839169edbba37e9ea561ea7d1896b7c
explicit Pretty_Tooltip.dismiss_all due to slightly changed focus mechanics;

diff -r d977e7eb7839 -r 5b7c4fb41511 src/Tools/jEdit/src/rich_text_area.scala
--- 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 {