--- a/src/Tools/jEdit/src/rich_text_area.scala Wed Apr 09 12:33:02 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Wed Apr 09 13:32:34 2014 +0200
@@ -168,12 +168,14 @@
robust_body(()) {
hyperlink_area.info match {
case Some(Text.Info(range, link)) =>
- try { text_area.moveCaretPosition(range.start) }
- catch {
- case _: ArrayIndexOutOfBoundsException =>
- case _: IllegalArgumentException =>
+ if (!link.external) {
+ try { text_area.moveCaretPosition(range.start) }
+ catch {
+ case _: ArrayIndexOutOfBoundsException =>
+ case _: IllegalArgumentException =>
+ }
+ text_area.requestFocus
}
- text_area.requestFocus
link.follow(view)
case None =>
}