# HG changeset patch
# User wenzelm
# Date 1482403096 -3600
# Node ID 6209e0f7a4e8c104d856662b5a44582ec16098ca
# Parent  65c8a7780538674e0f62e825aafad8591ca31e15
clarified modules;

diff -r 65c8a7780538 -r 6209e0f7a4e8 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Thu Dec 22 11:20:59 2016 +0100
+++ b/src/Pure/PIDE/resources.scala	Thu Dec 22 11:38:16 2016 +0100
@@ -53,6 +53,30 @@
 
 
 
+  /* source files of Isabelle/ML bootstrap */
+
+  def source_file(raw_name: String): Option[String] =
+  {
+    if (Path.is_wellformed(raw_name)) {
+      if (Path.is_valid(raw_name)) {
+        def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None
+
+        val path = Path.explode(raw_name)
+        val path1 =
+          if (path.is_absolute || path.is_current) check(path)
+          else {
+            check(Path.explode("~~/src/Pure") + path) orElse
+              (if (Isabelle_System.getenv("ML_SOURCES") == "") None
+               else check(Path.explode("$ML_SOURCES") + path))
+          }
+        Some(File.platform_path(path1 getOrElse path))
+      }
+      else None
+    }
+    else Some(raw_name)
+  }
+
+
   /* theory files */
 
   def loaded_files(syntax: Outer_Syntax, text: String): List[String] =
diff -r 65c8a7780538 -r 6209e0f7a4e8 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu Dec 22 11:20:59 2016 +0100
+++ b/src/Pure/System/isabelle_system.scala	Thu Dec 22 11:38:16 2016 +0100
@@ -161,21 +161,6 @@
 
   /** file-system operations **/
 
-  /* source files of Isabelle/ML bootstrap */
-
-  def source_file(path: Path): Option[Path] =
-  {
-    def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None
-
-    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))
-    }
-  }
-
-
   /* directories */
 
   def mkdirs(path: Path): Unit =
diff -r 65c8a7780538 -r 6209e0f7a4e8 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Thu Dec 22 11:20:59 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Thu Dec 22 11:38:16 2016 +0100
@@ -265,31 +265,19 @@
   def hyperlink_source_file(focus: Boolean, source_name: String, line1: Int, offset: Symbol.Offset)
     : Option[Hyperlink] =
   {
-    val opt_name =
-      if (Path.is_wellformed(source_name)) {
-        if (Path.is_valid(source_name)) {
-          val path = Path.explode(source_name)
-          Some(File.platform_path(Isabelle_System.source_file(path) getOrElse path))
-        }
-        else None
+    for (name <- PIDE.resources.source_file(source_name)) yield {
+      JEdit_Lib.jedit_buffer(name) match {
+        case Some(buffer) if offset > 0 =>
+          val pos =
+            JEdit_Lib.buffer_lock(buffer) {
+              (Line.Position.zero /:
+                (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
+                  zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_))
+            }
+          hyperlink_file(focus, Line.Node_Position(name, pos))
+        case _ =>
+          hyperlink_file(focus, Line.Node_Position(name, Line.Position((line1 - 1) max 0)))
       }
-      else Some(source_name)
-
-    opt_name match {
-      case Some(name) =>
-        JEdit_Lib.jedit_buffer(name) match {
-          case Some(buffer) if offset > 0 =>
-            val pos =
-              JEdit_Lib.buffer_lock(buffer) {
-                (Line.Position.zero /:
-                  (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
-                    zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_))
-              }
-            Some(hyperlink_file(focus, Line.Node_Position(name, pos)))
-          case _ =>
-            Some(hyperlink_file(focus, Line.Node_Position(name, Line.Position((line1 - 1) max 0))))
-        }
-      case None => None
     }
   }