# HG changeset patch
# User wenzelm
# Date 1492424445 -7200
# Node ID 331f09d9535ec2701fccc475a41859acf5650fae
# Parent  7847807b07ce0359c662c39b3e85a8dd45c289a2
tuned signature;

diff -r 7847807b07ce -r 331f09d9535e src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Apr 17 12:11:02 2017 +0200
+++ b/src/Pure/PIDE/command.scala	Mon Apr 17 12:20:45 2017 +0200
@@ -451,8 +451,7 @@
         val blobs =
           files.map(file =>
             (Exn.capture {
-              val name =
-                Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file)))
+              val name = Document.Node.Name(resources.append(node_name, Path.explode(file)))
               val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
               (name, blob)
             }).user_error)
diff -r 7847807b07ce -r 331f09d9535e src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Mon Apr 17 12:11:02 2017 +0200
+++ b/src/Pure/PIDE/rendering.scala	Mon Apr 17 12:20:45 2017 +0200
@@ -423,8 +423,8 @@
       rev_infos.filter(p => p._1 == important).reverse.map(_._2)
   }
 
-  def perhaps_append_file(dir: String, name: String): String =
-    if (Path.is_valid(name)) session.resources.append(dir, Path.explode(name)) else name
+  def perhaps_append_file(node_name: Document.Node.Name, name: String): String =
+    if (Path.is_valid(name)) session.resources.append(node_name, Path.explode(name)) else name
 
   def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] =
   {
@@ -451,7 +451,7 @@
             Some(info + (r0, true, XML.Text(txt1 + txt2)))
 
           case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) =>
-            val file = perhaps_append_file(snapshot.node_name.master_dir, name)
+            val file = perhaps_append_file(snapshot.node_name, name)
             val text =
               if (name == file) "file " + quote(file)
               else "path " + quote(name) + "\nfile " + quote(file)
diff -r 7847807b07ce -r 331f09d9535e src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Apr 17 12:11:02 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Mon Apr 17 12:20:45 2017 +0200
@@ -28,6 +28,9 @@
   def append(dir: String, source_path: Path): String =
     (Path.explode(dir) + source_path).expand.implode
 
+  def append(node_name: Document.Node.Name, source_path: Path): String =
+    append(node_name.master_dir, source_path)
+
 
   /* source files of Isabelle/ML bootstrap */
 
diff -r 7847807b07ce -r 331f09d9535e src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Mon Apr 17 12:11:02 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Mon Apr 17 12:20:45 2017 +0200
@@ -237,7 +237,7 @@
       range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
         {
           case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
-            val file = perhaps_append_file(snapshot.node_name.master_dir, name)
+            val file = perhaps_append_file(snapshot.node_name, name)
             Some(Line.Node_Range(file) :: links)
 
           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
diff -r 7847807b07ce -r 331f09d9535e src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Mon Apr 17 12:11:02 2017 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Apr 17 12:20:45 2017 +0200
@@ -195,8 +195,7 @@
             if (text == "" || text.endsWith("/")) (path, "")
             else (path.dir, path.base.implode)
 
-          val directory =
-            new JFile(PIDE.resources.append(rendering.snapshot.node_name.master_dir, dir))
+          val directory = new JFile(PIDE.resources.append(rendering.snapshot.node_name, dir))
           val files = directory.listFiles
           if (files == null) Nil
           else {
diff -r 7847807b07ce -r 331f09d9535e src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Mon Apr 17 12:11:02 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Mon Apr 17 12:20:45 2017 +0200
@@ -304,7 +304,7 @@
       range, Vector.empty, JEdit_Rendering.hyperlink_elements, _ =>
         {
           case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
-            val file = perhaps_append_file(snapshot.node_name.master_dir, name)
+            val file = perhaps_append_file(snapshot.node_name, name)
             val link = JEdit_Editor.hyperlink_file(true, file)
             Some(links :+ Text.Info(snapshot.convert(info_range), link))