src/Tools/jEdit/src/rich_text_area.scala
changeset 56494 1b74abf064e1
parent 56433 db69cb14f7ed
child 56496 46b29bb1c627
equal deleted inserted replaced
56493:1f660d858a75 56494:1b74abf064e1
   166   private val mouse_listener = new MouseAdapter {
   166   private val mouse_listener = new MouseAdapter {
   167     override def mouseClicked(e: MouseEvent) {
   167     override def mouseClicked(e: MouseEvent) {
   168       robust_body(()) {
   168       robust_body(()) {
   169         hyperlink_area.info match {
   169         hyperlink_area.info match {
   170           case Some(Text.Info(range, link)) =>
   170           case Some(Text.Info(range, link)) =>
   171             try { text_area.moveCaretPosition(range.start) }
   171             if (!link.external) {
   172             catch {
   172               try { text_area.moveCaretPosition(range.start) }
   173               case _: ArrayIndexOutOfBoundsException =>
   173               catch {
   174               case _: IllegalArgumentException =>
   174                 case _: ArrayIndexOutOfBoundsException =>
   175             }
   175                 case _: IllegalArgumentException =>
   176             text_area.requestFocus
   176               }
       
   177               text_area.requestFocus
       
   178             }
   177             link.follow(view)
   179             link.follow(view)
   178           case None =>
   180           case None =>
   179         }
   181         }
   180         active_area.text_info match {
   182         active_area.text_info match {
   181           case Some((text, Text.Info(_, markup))) =>
   183           case Some((text, Text.Info(_, markup))) =>