# HG changeset patch
# User wenzelm
# Date 1672485014 -3600
# Node ID 3dfc89c8dd7109913b4e1177b1ffa2e6e070c6e1
# Parent  18465808e61f763232f5ffc57e1b76875896e9fc
tuned signature;

diff -r 18465808e61f -r 3dfc89c8dd71 src/Pure/PIDE/protocol.scala
--- 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
       }
   }
diff -r 18465808e61f -r 3dfc89c8dd71 src/Pure/PIDE/resources.scala
--- 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
   }
diff -r 18465808e61f -r 3dfc89c8dd71 src/Pure/Thy/file_format.scala
--- 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)
     }
   }
 
diff -r 18465808e61f -r 3dfc89c8dd71 src/Tools/VSCode/src/vscode_resources.scala
--- 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)
       }
     }
 
diff -r 18465808e61f -r 3dfc89c8dd71 src/Tools/jEdit/src/jedit_resources.scala
--- 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)
       }
     }