# HG changeset patch
# User wenzelm
# Date 1396787426 -7200
# Node ID db69cb14f7eda78b96a302ba855aa25e8bf4fc58
# Parent  96b54a96b1177b14db9c9a26301ffd590704d6d6
prepare "back" position for Navigator, before following hyperlink;

diff -r 96b54a96b117 -r db69cb14f7ed 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 =>
         }