# HG changeset patch
# User wenzelm
# Date 1672610080 -3600
# Node ID 39db5e268aaff0751dc0cd951f02adc3291460c9
# Parent  3bd08d0432d72129b66adc10891aa5664718424b
tuned signature, following Url.append_path;

diff -r 3bd08d0432d7 -r 39db5e268aaf src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sun Jan 01 22:01:53 2023 +0100
+++ b/src/Pure/PIDE/command.scala	Sun Jan 01 22:54:40 2023 +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.master_dir, src_path))
+              val name = Document.Node.Name(resources.append_path(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 3bd08d0432d7 -r 39db5e268aaf src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Sun Jan 01 22:01:53 2023 +0100
+++ b/src/Pure/PIDE/headless.scala	Sun Jan 01 22:54:40 2023 +0100
@@ -306,7 +306,7 @@
       val dep_theories_set = dep_theories.toSet
       val dep_files =
         for (path <- dependencies.loaded_files)
-          yield Document.Node.Name(resources.append("", path))
+          yield Document.Node.Name(resources.append_path("", path))
 
       val use_theories_state = {
         val dep_graph = dependencies.theory_graph
diff -r 3bd08d0432d7 -r 39db5e268aaf src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Sun Jan 01 22:01:53 2023 +0100
+++ b/src/Pure/PIDE/rendering.scala	Sun Jan 01 22:54:40 2023 +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.master_dir, dir))
+        val directory = new JFile(session.resources.append_path(snapshot.node_name.master_dir, dir))
         val files = directory.listFiles
         if (files == null) Nil
         else {
@@ -616,7 +616,7 @@
   }
 
   def perhaps_append_file(node_name: Document.Node.Name, name: String): String =
-    if (Path.is_valid(name)) session.resources.append(node_name.master_dir, Path.explode(name))
+    if (Path.is_valid(name)) session.resources.append_path(node_name.master_dir, Path.explode(name))
     else name
 
   def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] = {
diff -r 3bd08d0432d7 -r 39db5e268aaf src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sun Jan 01 22:01:53 2023 +0100
+++ b/src/Pure/PIDE/resources.scala	Sun Jan 01 22:54:40 2023 +0100
@@ -72,12 +72,12 @@
 
   def migrate_name(name: Document.Node.Name): Document.Node.Name = name
 
-  def append(dir: String, source_path: Path): String =
+  def append_path(dir: String, source_path: Path): String =
     (Path.explode(dir) + source_path).expand.implode
 
   def file_node(file: Path, dir: String = "", theory: String = ""): Document.Node.Name = {
-    val node = append(dir, file)
-    val master_dir = append(dir, file.dir)
+    val node = append_path(dir, file)
+    val master_dir = append_path(dir, file.dir)
     Document.Node.Name(node, master_dir = master_dir, theory = theory)
   }
 
diff -r 3bd08d0432d7 -r 39db5e268aaf src/Pure/Thy/file_format.scala
--- a/src/Pure/Thy/file_format.scala	Sun Jan 01 22:01:53 2023 +0100
+++ b/src/Pure/Thy/file_format.scala	Sun Jan 01 22:54:40 2023 +0100
@@ -87,7 +87,7 @@
       if detect(name.node) && theory_suffix.nonEmpty
     }
     yield {
-      val node = resources.append(name.node, Path.explode(theory_suffix))
+      val node = resources.append_path(name.node, Path.explode(theory_suffix))
       Document.Node.Name(node, master_dir = name.master_dir, theory = theory)
     }
   }
diff -r 3bd08d0432d7 -r 39db5e268aaf src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Sun Jan 01 22:01:53 2023 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sun Jan 01 22:54:40 2023 +0100
@@ -103,7 +103,7 @@
   override def migrate_name(standard_name: Document.Node.Name): Document.Node.Name =
     node_name(Path.explode(standard_name.node).canonical_file)
 
-  override def append(dir: String, source_path: Path): String = {
+  override def append_path(dir: String, source_path: Path): String = {
     val path = source_path.expand
     if (dir == "" || path.is_absolute) File.platform_path(path)
     else if (path.is_current) dir
diff -r 3bd08d0432d7 -r 39db5e268aaf src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 01 22:01:53 2023 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 01 22:54:40 2023 +0100
@@ -53,7 +53,7 @@
   override def migrate_name(standard_name: Document.Node.Name): Document.Node.Name =
     node_name(File.platform_path(Path.explode(standard_name.node).canonical))
 
-  override def append(dir: String, source_path: Path): String = {
+  override def append_path(dir: String, source_path: Path): String = {
     val path = source_path.expand
     if (dir == "" || path.is_absolute) {
       MiscUtilities.resolveSymlinks(File.platform_path(path))