# HG changeset patch
# User wenzelm
# Date 1671273193 -3600
# Node ID b7546c25e4f09c80c06064309478c8b2ef35e539
# Parent  762406d791f46f789e86dfa8978fe5a91c2762ed
clarified signature;

diff -r 762406d791f4 -r b7546c25e4f0 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sat Dec 17 11:25:19 2022 +0100
+++ b/src/Pure/PIDE/command.scala	Sat Dec 17 11:33:13 2022 +0100
@@ -464,7 +464,7 @@
           loaded_files.files.map(file =>
             (Exn.capture {
               val src_path = Path.explode(file)
-              val name = Document.Node.Name(resources.append(node_name, src_path))
+              val name = Document.Node.Name(resources.append(node_name.master_dir, src_path))
               val content = get_blob(name).map(blob => (blob.bytes.sha1_digest, blob.chunk))
               Blob(name, src_path, content)
             }).user_error)
diff -r 762406d791f4 -r b7546c25e4f0 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Sat Dec 17 11:25:19 2022 +0100
+++ b/src/Pure/PIDE/rendering.scala	Sat Dec 17 11:33:13 2022 +0100
@@ -348,7 +348,7 @@
           if (text == "" || text.endsWith("/")) (path, "")
           else (path.dir, path.file_name)
 
-        val directory = new JFile(session.resources.append(snapshot.node_name, dir))
+        val directory = new JFile(session.resources.append(snapshot.node_name.master_dir, dir))
         val files = directory.listFiles
         if (files == null) Nil
         else {
@@ -616,7 +616,8 @@
   }
 
   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
+    if (Path.is_valid(name)) session.resources.append(node_name.master_dir, Path.explode(name))
+    else name
 
   def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] = {
     val results =
diff -r 762406d791f4 -r b7546c25e4f0 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sat Dec 17 11:25:19 2022 +0100
+++ b/src/Pure/PIDE/resources.scala	Sat Dec 17 11:33:13 2022 +0100
@@ -74,9 +74,6 @@
   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)
-
   def file_node(file: Path, dir: String = "", theory: String = ""): Document.Node.Name = {
     val node = append(dir, file)
     val master_dir = append(dir, file.dir)