# HG changeset patch
# User wenzelm
# Date 1397043154 -7200
# Node ID 1b74abf064e1c8168117df898dad71c55b55b7bc
# Parent  1f660d858a75dbc06837c75a4f8df3e8a888b5cd
avoid confusion about pointless cursor movement with external links;

diff -r 1f660d858a75 -r 1b74abf064e1 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Wed Apr 09 12:33:02 2014 +0200
+++ b/src/Pure/PIDE/editor.scala	Wed Apr 09 13:32:34 2014 +0200
@@ -22,7 +22,10 @@
   def insert_overlay(command: Command, fn: String, args: List[String]): Unit
   def remove_overlay(command: Command, fn: String, args: List[String]): Unit
 
-  abstract class Hyperlink { def follow(context: Context): Unit }
+  abstract class Hyperlink {
+    def external: Boolean
+    def follow(context: Context): Unit
+  }
   def hyperlink_command(
     snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0): Option[Hyperlink]
 }
diff -r 1f660d858a75 -r 1b74abf064e1 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Apr 09 12:33:02 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Apr 09 13:32:34 2014 +0200
@@ -161,6 +161,7 @@
 
   def hyperlink_url(name: String): Hyperlink =
     new Hyperlink {
+      val external = true
       def follow(view: View) =
         default_thread_pool.submit(() =>
           try { Isabelle_System.open(name) }
@@ -173,6 +174,7 @@
 
   def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
     new Hyperlink {
+      val external = false
       def follow(view: View) = goto_file(view, name, line, column)
       override def toString: String = "file " + quote(name)
     }
diff -r 1f660d858a75 -r 1b74abf064e1 src/Tools/jEdit/src/rich_text_area.scala
--- 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 =>
         }