# HG changeset patch
# User wenzelm
# Date 1483898906 -3600
# Node ID d53696aed874cadea6fdf2eb7e8968a75027b13e
# Parent  d67253005c0c9569c245c6cedacb022f24d6aeb8
added node_name(String): imitate jEdit buffer operations;
more uniform get_file_content for external source file references;

diff -r d67253005c0c -r d53696aed874 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Sun Jan 08 17:53:44 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Sun Jan 08 19:08:26 2017 +0100
@@ -90,14 +90,17 @@
     }
     yield {
       Line.Node_Range(file.getPath,
-        resources.get_file_content(file) match {
-          case Some(text) if range.start > 0 =>
-            val chunk = Symbol.Text_Chunk(text)
-            val doc = Line.Document(text, resources.text_length)
-            doc.range(chunk.decode(range))
-          case _ =>
-            Line.Range(Line.Position((line1 - 1) max 0))
-        })
+        if (range.start > 0) {
+          resources.get_file_content(file) match {
+            case Some(text) =>
+              val chunk = Symbol.Text_Chunk(text)
+              val doc = Line.Document(text, resources.text_length)
+              doc.range(chunk.decode(range))
+            case _ =>
+              Line.Range(Line.Position((line1 - 1) max 0))
+          }
+        }
+        else Line.Range(Line.Position((line1 - 1) max 0)))
     }
   }
 
diff -r d67253005c0c -r d53696aed874 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Sun Jan 08 17:53:44 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Sun Jan 08 19:08:26 2017 +0100
@@ -250,19 +250,22 @@
     : Option[Hyperlink] =
   {
     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) {
+      def hyperlink(pos: Line.Position) =
+        hyperlink_file(focus, Line.Node_Position(name, pos))
+
+      if (offset > 0) {
+        PIDE.resources.get_file_content(PIDE.resources.node_name(name)) match {
+          case Some(text) =>
+            hyperlink(
               (Line.Position.zero /:
-                (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
+                (Symbol.iterator(text).
                   zipWithIndex.takeWhile(p => p._2 < offset - 1).
-                  map(_._1)))(_.advance(_, Text.Length))
-            }
-          hyperlink_file(focus, Line.Node_Position(name, pos))
-        case _ =>
-          hyperlink_file(focus, Line.Node_Position(name, Line.Position((line1 - 1) max 0)))
+                  map(_._1)))(_.advance(_, Text.Length)))
+          case None =>
+            hyperlink(Line.Position((line1 - 1) max 0))
+        }
       }
+      else hyperlink(Line.Position((line1 - 1) max 0))
     }
   }
 
diff -r d67253005c0c -r d53696aed874 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 08 17:53:44 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 08 19:08:26 2017 +0100
@@ -43,6 +43,15 @@
     Document.Node.Name(node, master_dir, theory)
   }
 
+  def node_name(path: String): Document.Node.Name =
+  {
+    val vfs = VFSManager.getVFSForPath(path)
+    val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
+    val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
+    val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
+    Document.Node.Name(node, master_dir, theory)
+  }
+
   def theory_node_name(buffer: Buffer): Option[Document.Node.Name] =
   {
     val name = node_name(buffer)
@@ -79,14 +88,20 @@
     catch { case ERROR(_) => None }
   }
 
+  def get_file_content(node_name: Document.Node.Name): Option[String] =
+    Document_Model.get(node_name) match {
+      case Some(model: Buffer_Model) => Some(JEdit_Lib.buffer_text(model.buffer))
+      case Some(model: File_Model) => Some(model.content.text)
+      case None => read_file_content(node_name)
+    }
+
   override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   {
     GUI_Thread.now {
       Document_Model.get(name) match {
-        case Some(buffer_model: Buffer_Model) =>
-          val buffer = buffer_model.buffer
-          JEdit_Lib.buffer_lock(buffer) { Some(f(JEdit_Lib.buffer_reader(buffer))) }
-        case Some(file_model: File_Model) => Some(f(Scan.char_reader(file_model.content.text)))
+        case Some(model: Buffer_Model) =>
+          JEdit_Lib.buffer_lock(model.buffer) { Some(f(JEdit_Lib.buffer_reader(model.buffer))) }
+        case Some(model: File_Model) => Some(f(Scan.char_reader(model.content.text)))
         case None => None
       }
     } getOrElse {