--- 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)
}
}
}
--- 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
--- 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))
}
}