prepare "back" position for Navigator, before following hyperlink;
authorwenzelm
Sun, 06 Apr 2014 14:30:26 +0200
changeset 56433 db69cb14f7ed
parent 56432 96b54a96b117
child 56434 7acc933bd7cc
prepare "back" position for Navigator, before following hyperlink;
src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Apr 05 23:56:21 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sun Apr 06 14:30:26 2014 +0200
@@ -167,7 +167,13 @@
     override def mouseClicked(e: MouseEvent) {
       robust_body(()) {
         hyperlink_area.info match {
-          case Some(Text.Info(_, link)) =>
+          case Some(Text.Info(range, link)) =>
+            try { text_area.moveCaretPosition(range.start) }
+            catch {
+              case _: ArrayIndexOutOfBoundsException =>
+              case _: IllegalArgumentException =>
+            }
+            text_area.requestFocus
             link.follow(view)
           case None =>
         }