--- a/src/Pure/PIDE/resources.scala Mon Jan 02 12:34:20 2023 +0100
+++ b/src/Pure/PIDE/resources.scala Mon Jan 02 12:45:24 2023 +0100
@@ -75,9 +75,6 @@
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 =
- Document.Node.Name(append_path(dir, file), theory = theory)
-
/* source files of Isabelle/ML bootstrap */
@@ -158,8 +155,8 @@
case Some(info) => info.dirs
case None => Nil
}
- dirs.collectFirst({
- case dir if (dir + thy_file).is_file => file_node(dir + thy_file, theory = theory) })
+ dirs.collectFirst { case dir if (dir + thy_file).is_file =>
+ Document.Node.Name(append_path("", dir + thy_file), theory = theory) }
}
def import_name(qualifier: String, dir: String, s: String): Document.Node.Name = {
@@ -175,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 file_node(Path.explode(s).thy, dir = dir, theory = theory)
+ else Document.Node.Name(append_path(dir, Path.explode(s).thy), theory = theory)
}
}
}