--- a/src/Pure/PIDE/protocol.scala Sat Dec 31 11:58:45 2022 +0100
+++ b/src/Pure/PIDE/protocol.scala Sat Dec 31 12:10:14 2022 +0100
@@ -28,7 +28,7 @@
case (Markup.Name(name), Position.File(file), Position.Id(id))
if Path.is_wellformed(file) =>
val master_dir = Path.explode(file).dir.implode
- Some((Document.Node.Name(file, master_dir, name), id))
+ Some((Document.Node.Name(file, master_dir = master_dir, theory = name), id))
case _ => None
}
}
--- a/src/Pure/PIDE/resources.scala Sat Dec 31 11:58:45 2022 +0100
+++ b/src/Pure/PIDE/resources.scala Sat Dec 31 12:10:14 2022 +0100
@@ -78,11 +78,11 @@
def file_node(file: Path, dir: String = "", theory: String = ""): Document.Node.Name = {
val node = append(dir, file)
val master_dir = append(dir, file.dir)
- Document.Node.Name(node, master_dir, theory)
+ Document.Node.Name(node, master_dir = master_dir, theory = theory)
}
def loaded_theory_node(theory: String): Document.Node.Name =
- Document.Node.Name(theory, "", theory)
+ Document.Node.Name(theory, theory = theory)
/* source files of Isabelle/ML bootstrap */
@@ -141,7 +141,7 @@
for {
(name, theory) <- Thy_Header.ml_roots
path = (pure_dir + Path.explode(name)).expand
- node_name = Document.Node.Name(path.implode, path.dir.implode, theory)
+ node_name = Document.Node.Name(path.implode, master_dir = path.dir.implode, theory = theory)
file <- loaded_files(syntax, node_name, load_commands(syntax, node_name)())
} yield file
}
--- a/src/Pure/Thy/file_format.scala Sat Dec 31 11:58:45 2022 +0100
+++ b/src/Pure/Thy/file_format.scala Sat Dec 31 12:10:14 2022 +0100
@@ -85,7 +85,7 @@
}
yield {
val thy_node = resources.append(name.node, Path.explode(theory_suffix))
- Document.Node.Name(thy_node, name.master_dir, thy)
+ Document.Node.Name(thy_node, master_dir = name.master_dir, theory = thy)
}
}
--- a/src/Tools/VSCode/src/vscode_resources.scala Sat Dec 31 11:58:45 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Sat Dec 31 12:10:14 2022 +0100
@@ -96,7 +96,7 @@
if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
else {
val master_dir = file.getParent
- Document.Node.Name(node, master_dir, theory)
+ Document.Node.Name(node, master_dir = master_dir, theory = theory)
}
}
--- a/src/Tools/jEdit/src/jedit_resources.scala Sat Dec 31 11:58:45 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Sat Dec 31 12:10:14 2022 +0100
@@ -38,7 +38,7 @@
if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
else {
val master_dir = vfs.getParentOfPath(path)
- Document.Node.Name(node, master_dir, theory)
+ Document.Node.Name(node, master_dir = master_dir, theory = theory)
}
}