# HG changeset patch
# User wenzelm
# Date 1672761223 -3600
# Node ID f405fcc3db3383274df32c3c0dd501ff224ce7f3
# Parent  c2932487360dd7d45d00a149c330a5b079b57e38
clarified signature: avoid somewhat fragile Document.Node.Name.master_dir_path;

diff -r c2932487360d -r f405fcc3db33 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Tue Jan 03 16:14:17 2023 +0100
+++ b/src/Pure/PIDE/headless.scala	Tue Jan 03 16:53:43 2023 +0100
@@ -304,9 +304,7 @@
       }
       val dep_theories = dependencies.theories
       val dep_theories_set = dep_theories.toSet
-      val dep_files =
-        for (path <- dependencies.loaded_files)
-          yield Document.Node.Name(resources.append_path("", path))
+      val dep_files = dependencies.loaded_files
 
       val use_theories_state = {
         val dep_graph = dependencies.theory_graph
diff -r c2932487360d -r f405fcc3db33 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Jan 03 16:14:17 2023 +0100
+++ b/src/Pure/PIDE/resources.scala	Tue Jan 03 16:53:43 2023 +0100
@@ -121,19 +121,18 @@
     syntax: Outer_Syntax,
     name: Document.Node.Name,
     spans: List[Command_Span.Span]
-  ) : List[Path] = {
-    val dir = name.master_dir_path
-    for { span <- spans; file <- span.loaded_files(syntax).files }
-      yield (dir + Path.explode(file)).expand
+  ) : List[Document.Node.Name] = {
+    for (span <- spans; file <- span.loaded_files(syntax).files)
+      yield Document.Node.Name(append_path(name.master_dir, Path.explode(file)))
   }
 
-  def pure_files(syntax: Outer_Syntax): List[Path] =
+  def pure_files(syntax: Outer_Syntax): List[Document.Node.Name] =
     (for {
-      (name, theory) <- Thy_Header.ml_roots.iterator
-      node = append_path("~~/src/Pure", Path.explode(name))
+      (file, theory) <- Thy_Header.ml_roots.iterator
+      node = append_path("~~/src/Pure", Path.explode(file))
       node_name = Document.Node.Name(node, theory = theory)
-      file <- loaded_files(syntax, node_name, load_commands(syntax, node_name)()).iterator
-    } yield file).toList
+      name <- loaded_files(syntax, node_name, load_commands(syntax, node_name)()).iterator
+    } yield name).toList
 
   def global_theory(theory: String): Boolean =
     sessions_structure.global_theories.isDefinedAt(theory)
@@ -414,7 +413,7 @@
     def loaded_files(
       name: Document.Node.Name,
       spans: List[Command_Span.Span]
-    ) : (String, List[Path]) = {
+    ) : (String, List[Document.Node.Name]) = {
       val theory = name.theory
       val syntax = get_syntax(name)
       val files1 = resources.loaded_files(syntax, name, spans)
@@ -422,7 +421,7 @@
       (theory, files1 ::: files2)
     }
 
-    def loaded_files: List[Path] =
+    def loaded_files: List[Document.Node.Name] =
       for {
         (name, spans) <- load_commands
         file <- loaded_files(name, spans)._2
diff -r c2932487360d -r f405fcc3db33 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Jan 03 16:14:17 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Jan 03 16:53:43 2023 +0100
@@ -357,8 +357,11 @@
             val theory_load_commands =
               (for ((name, span) <- load_commands.iterator) yield name.theory -> span).toMap
 
-            val loaded_files =
-              load_commands.map({ case (name, spans) => dependencies.loaded_files(name, spans) })
+            val loaded_files: List[(String, List[Path])] =
+              for ((name, spans) <- load_commands) yield {
+                val (theory, files) = dependencies.loaded_files(name, spans)
+                theory -> files.map(file => Path.explode(file.node))
+              }
 
             val session_files =
               (theory_files ::: loaded_files.flatMap(_._2) :::