# HG changeset patch
# User wenzelm
# Date 1672658948 -3600
# Node ID f95ed5a0600c7ff8bfd358705841e19889678ff8
# Parent  6e1bf28d5a80c21e7dc8ad3a3e9c24127497f721
clarified signature: uniform master_dir instead of separate field;

diff -r 6e1bf28d5a80 -r f95ed5a0600c src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Jan 02 11:57:57 2023 +0100
+++ b/src/Pure/PIDE/document.scala	Mon Jan 02 12:29:08 2023 +0100
@@ -91,11 +91,9 @@
     def bad_header(msg: String): Header = Header(errors = List(msg))
 
     object Name {
-      def apply(node: String, master_dir: String = "", theory: String = ""): Name =
-        new Name(node, master_dir, theory)
+      def apply(node: String, theory: String = ""): Name = new Name(node, theory)
 
-      def loaded_theory(theory: String): Document.Node.Name =
-        Name(theory, theory = theory)
+      def loaded_theory(theory: String): Document.Node.Name = Name(theory, theory = theory)
 
       val empty: Name = Name("")
 
@@ -109,7 +107,7 @@
         Graph.make(entries, converse = true)(Ordering)
     }
 
-    final class Name private(val node: String, val master_dir: String, val theory: String) {
+    final class Name private(val node: String, val theory: String) {
       override def hashCode: Int = node.hashCode
       override def equals(that: Any): Boolean =
         that match {
@@ -120,6 +118,8 @@
       def file_name: String = Url.get_base_name(node).getOrElse("")
 
       def path: Path = Path.explode(File.standard_path(node))
+
+      def master_dir: String = Url.strip_base_name(node).getOrElse("")
       def master_dir_path: Path = Path.explode(File.standard_path(master_dir))
 
       def is_theory: Boolean = theory.nonEmpty
diff -r 6e1bf28d5a80 -r f95ed5a0600c src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Mon Jan 02 11:57:57 2023 +0100
+++ b/src/Pure/PIDE/protocol.scala	Mon Jan 02 12:29:08 2023 +0100
@@ -26,9 +26,7 @@
     def unapply(props: Properties.T): Option[(Document.Node.Name, Document_ID.Exec)] =
       (props, props, props) match {
         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 = master_dir, theory = name), id))
+        if Path.is_wellformed(file) => Some((Document.Node.Name(file, theory = name), id))
         case _ => None
       }
   }
diff -r 6e1bf28d5a80 -r f95ed5a0600c src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Jan 02 11:57:57 2023 +0100
+++ b/src/Pure/PIDE/resources.scala	Mon Jan 02 12:29:08 2023 +0100
@@ -75,11 +75,8 @@
   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 = {
-    val node = append_path(dir, file)
-    val master_dir = append_path(dir, file.dir)
-    Document.Node.Name(node, master_dir = master_dir, theory = theory)
-  }
+  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 */
@@ -138,7 +135,7 @@
     for {
       (name, theory) <- Thy_Header.ml_roots
       path = (pure_dir + Path.explode(name)).expand
-      node_name = Document.Node.Name(path.implode, master_dir = path.dir.implode, theory = theory)
+      node_name = Document.Node.Name(path.implode, theory = theory)
       file <- loaded_files(syntax, node_name, load_commands(syntax, node_name)())
     } yield file
   }
diff -r 6e1bf28d5a80 -r f95ed5a0600c src/Pure/Thy/file_format.scala
--- a/src/Pure/Thy/file_format.scala	Mon Jan 02 11:57:57 2023 +0100
+++ b/src/Pure/Thy/file_format.scala	Mon Jan 02 12:29:08 2023 +0100
@@ -88,8 +88,7 @@
     }
     yield {
       val node = resources.append_path(name.node, Path.explode(theory_suffix))
-      val master_dir = Url.strip_base_name(node).getOrElse("")
-      Document.Node.Name(node, master_dir = master_dir, theory = theory)
+      Document.Node.Name(node, theory = theory)
     }
   }
 
diff -r 6e1bf28d5a80 -r f95ed5a0600c src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Mon Jan 02 11:57:57 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Mon Jan 02 12:29:08 2023 +0100
@@ -33,8 +33,7 @@
       val master_dir =
         Url.strip_base_name(thy_file).getOrElse(
           error("Cannot determine theory master directory: " + quote(thy_file)))
-      val node_name =
-        Document.Node.Name(thy_file, master_dir = master_dir, theory = theory_context.theory)
+      val node_name = Document.Node.Name(thy_file, theory = theory_context.theory)
 
       val results =
         Command.Results.make(
diff -r 6e1bf28d5a80 -r f95ed5a0600c src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Jan 02 11:57:57 2023 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Jan 02 12:29:08 2023 +0100
@@ -94,10 +94,7 @@
       val node = file.getPath
       val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
       if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
-      else {
-        val master_dir = file.getParent
-        Document.Node.Name(node, master_dir = master_dir, theory = theory)
-      }
+      else Document.Node.Name(node, theory = theory)
     }
 
   override def migrate_name(standard_name: Document.Node.Name): Document.Node.Name =
diff -r 6e1bf28d5a80 -r f95ed5a0600c src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Jan 02 11:57:57 2023 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Jan 02 12:29:08 2023 +0100
@@ -36,10 +36,7 @@
       val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
       val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
       if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
-      else {
-        val master_dir = vfs.getParentOfPath(path)
-        Document.Node.Name(node, master_dir = master_dir, theory = theory)
-      }
+      else Document.Node.Name(node, theory = theory)
     }
 
   def node_name(buffer: Buffer): Document.Node.Name =