# HG changeset patch
# User wenzelm
# Date 1672661378 -3600
# Node ID 56c926de7ea6dadf85a000321a9f79092d5165e8
# Parent  13b2d8961f8ae6e2e66932a6ff0ed4a1e02fc1f6
tuned signature, following Url.append_path;

diff -r 13b2d8961f8a -r 56c926de7ea6 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Jan 02 12:56:31 2023 +0100
+++ b/src/Pure/PIDE/resources.scala	Mon Jan 02 13:09:38 2023 +0100
@@ -72,8 +72,8 @@
 
   def migrate_name(name: Document.Node.Name): Document.Node.Name = name
 
-  def append_path(dir: String, source_path: Path): String =
-    (Path.explode(dir) + source_path).expand.implode
+  def append_path(prefix: String, source_path: Path): String =
+    (Path.explode(prefix) + source_path).expand.implode
 
 
   /* source files of Isabelle/ML bootstrap */
@@ -159,7 +159,7 @@
       Document.Node.Name(append_path("", dir + thy_file), theory = theory) }
   }
 
-  def import_name(qualifier: String, dir: String, s: String): Document.Node.Name = {
+  def import_name(qualifier: String, prefix: String, s: String): Document.Node.Name = {
     val theory = theory_name(qualifier, Thy_Header.import_name(s))
     val literal_import =
       literal_theory(theory) && qualifier != sessions_structure.theory_qualifier(theory)
@@ -172,7 +172,7 @@
         case Some(node_name) => node_name
         case None =>
           if (Url.is_base_name(s) && literal_theory(s)) Document.Node.Name.loaded_theory(theory)
-          else Document.Node.Name(append_path(dir, Path.explode(s).thy), theory = theory)
+          else Document.Node.Name(append_path(prefix, Path.explode(s).thy), theory = theory)
       }
     }
   }
diff -r 13b2d8961f8a -r 56c926de7ea6 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Jan 02 12:56:31 2023 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Jan 02 13:09:38 2023 +0100
@@ -100,14 +100,14 @@
   override def migrate_name(standard_name: Document.Node.Name): Document.Node.Name =
     node_name(Path.explode(standard_name.node).canonical_file)
 
-  override def append_path(dir: String, source_path: Path): String = {
+  override def append_path(prefix: 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
-    else if (path.is_basic && !dir.endsWith("/") && !dir.endsWith(JFile.separator))
-      dir + JFile.separator + File.platform_path(path)
-    else if (path.is_basic) dir + File.platform_path(path)
-    else File.absolute_name(new JFile(dir + JFile.separator + File.platform_path(path)))
+    if (prefix == "" || path.is_absolute) File.platform_path(path)
+    else if (path.is_current) prefix
+    else if (path.is_basic && !prefix.endsWith("/") && !prefix.endsWith(JFile.separator))
+      prefix + JFile.separator + File.platform_path(path)
+    else if (path.is_basic) prefix + File.platform_path(path)
+    else File.absolute_name(new JFile(prefix + JFile.separator + File.platform_path(path)))
   }
 
   def get_models(): Iterable[VSCode_Model] = state.value.models.values
diff -r 13b2d8961f8a -r 56c926de7ea6 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Jan 02 12:56:31 2023 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Jan 02 13:09:38 2023 +0100
@@ -50,19 +50,19 @@
   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_path(dir: String, source_path: Path): String = {
+  override def append_path(prefix: String, source_path: Path): String = {
     val path = source_path.expand
-    if (dir == "" || path.is_absolute) {
+    if (prefix == "" || path.is_absolute) {
       MiscUtilities.resolveSymlinks(File.platform_path(path))
     }
-    else if (path.is_current) dir
+    else if (path.is_current) prefix
     else {
-      val vfs = VFSManager.getVFSForPath(dir)
+      val vfs = VFSManager.getVFSForPath(prefix)
       if (vfs.isInstanceOf[FileVFS]) {
         MiscUtilities.resolveSymlinks(
-          vfs.constructPath(dir, File.platform_path(path)))
+          vfs.constructPath(prefix, File.platform_path(path)))
       }
-      else vfs.constructPath(dir, File.standard_path(path))
+      else vfs.constructPath(prefix, File.standard_path(path))
     }
   }