--- 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 =>
}