equal
deleted
inserted
replaced
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))) => |