# HG changeset patch
# User wenzelm
# Date 1393839718 -3600
# Node ID 1421394576536ec9cac2f9bf1af749a17436bd42
# Parent  7f229b0212fe3b581b9b1e05268bc14475f151ce
tuned signature;

diff -r 7f229b0212fe -r 142139457653 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Mon Mar 03 03:13:45 2014 +0100
+++ b/src/Pure/PIDE/editor.scala	Mon Mar 03 10:41:58 2014 +0100
@@ -23,9 +23,7 @@
   def remove_overlay(command: Command, fn: String, args: List[String]): Unit
 
   abstract class Hyperlink { def follow(context: Context): Unit }
-  def hyperlink_url(name: String): Hyperlink
-  def hyperlink_file(file_name: String, line: Int = 0, column: Int = 0): Hyperlink
   def hyperlink_command(
-    snapshot: Document.Snapshot, command: Command, offset: Text.Offset = 0): Option[Hyperlink]
+    snapshot: Document.Snapshot, command: Command, raw_offset: Text.Offset = 0): Option[Hyperlink]
 }
 
diff -r 7f229b0212fe -r 142139457653 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Mar 03 03:13:45 2014 +0100
+++ b/src/Pure/System/isabelle_system.scala	Mon Mar 03 10:41:58 2014 +0100
@@ -212,7 +212,8 @@
     if (path.is_absolute || path.is_current) check(path)
     else {
       check(Path.explode("~~/src/Pure") + path) orElse
-        (if (getenv("ML_SOURCES") == "") None else check(Path.explode("$ML_SOURCES") + path))
+        (if (getenv("ML_SOURCES") == "") None
+         else check(Path.explode("$ML_SOURCES") + path))
     }
   }
 
diff -r 7f229b0212fe -r 142139457653 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Mar 03 03:13:45 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Mar 03 10:41:58 2014 +0100
@@ -142,20 +142,6 @@
     }
   }
 
-  override def hyperlink_url(name: String): Hyperlink =
-    new Hyperlink {
-      def follow(view: View) =
-        default_thread_pool.submit(() =>
-          try { Isabelle_System.open(name) }
-          catch {
-            case exn: Throwable =>
-              GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
-          })
-    }
-
-  override def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
-    new Hyperlink { def follow(view: View) = goto(view, name, line, column) }
-
   override def hyperlink_command(snapshot: Document.Snapshot, command: Command, raw_offset: Int = 0)
     : Option[Hyperlink] =
   {
@@ -174,4 +160,35 @@
       }
     }
   }
+
+  def hyperlink_command_id(
+    snapshot: Document.Snapshot,
+    id: Document_ID.Generic,
+    raw_offset: Text.Offset): Option[Hyperlink] =
+  {
+    snapshot.state.find_command(snapshot.version, id) match {
+      case Some((node, command)) => hyperlink_command(snapshot, command, raw_offset)
+      case None => None
+    }
+  }
+
+  def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
+    new Hyperlink { def follow(view: View) = goto(view, name, line, column) }
+
+  def hyperlink_source_file(name: String, line: Int): Option[Hyperlink] =
+    if (Path.is_ok(name))
+      Isabelle_System.source_file(Path.explode(name)).map(path =>
+        hyperlink_file(Isabelle_System.platform_path(path), line))
+    else None
+
+  def hyperlink_url(name: String): Hyperlink =
+    new Hyperlink {
+      def follow(view: View) =
+        default_thread_pool.submit(() =>
+          try { Isabelle_System.open(name) }
+          catch {
+            case exn: Throwable =>
+              GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
+          })
+    }
 }
diff -r 7f229b0212fe -r 142139457653 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 03:13:45 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 10:41:58 2014 +0100
@@ -327,20 +327,6 @@
 
   /* hyperlinks */
 
-  private def hyperlink_file(line: Int, name: String): Option[PIDE.editor.Hyperlink] =
-    if (Path.is_ok(name))
-      Isabelle_System.source_file(Path.explode(name)).map(path =>
-        PIDE.editor.hyperlink_file(Isabelle_System.platform_path(path), line))
-    else None
-
-  private def hyperlink_command(id: Document_ID.Generic, offset: Text.Offset)
-      : Option[PIDE.editor.Hyperlink] =
-    snapshot.state.find_command(snapshot.version, id) match {
-      case Some((node, command)) =>
-        PIDE.editor.hyperlink_command(snapshot, command, offset)
-      case None => None
-    }
-
   def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
   {
     snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
@@ -364,8 +350,10 @@
 
             val opt_link =
               props match {
-                case Position.Def_Line_File(line, name) => hyperlink_file(line, name)
-                case Position.Def_Id_Offset(id, offset) => hyperlink_command(id, offset)
+                case Position.Def_Line_File(line, name) =>
+                  PIDE.editor.hyperlink_source_file(name, line)
+                case Position.Def_Id_Offset(id, offset) =>
+                  PIDE.editor.hyperlink_command_id(snapshot, id, offset)
                 case _ => None
               }
             opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
@@ -373,8 +361,10 @@
           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
             val opt_link =
               props match {
-                case Position.Line_File(line, name) => hyperlink_file(line, name)
-                case Position.Id_Offset(id, offset) => hyperlink_command(id, offset)
+                case Position.Line_File(line, name) =>
+                  PIDE.editor.hyperlink_source_file(name, line)
+                case Position.Id_Offset(id, offset) =>
+                  PIDE.editor.hyperlink_command_id(snapshot, id, offset)
                 case _ => None
               }
             opt_link.map(link => links :+ (Text.Info(snapshot.convert(info_range), link)))