# HG changeset patch
# User wenzelm
# Date 1660937113 -7200
# Node ID 4da80799352f4480df4a4b59fae5e01cea185d45
# Parent  540aad9405b15f913f6d27443f5aea9803827a61
more robust treatment of Document.Node.Name, following stored data;

diff -r 540aad9405b1 -r 4da80799352f src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Aug 19 21:04:14 2022 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Aug 19 21:25:13 2022 +0200
@@ -591,7 +591,7 @@
 
     def xml_markup_blobs(
       elements: Markup.Elements = Markup.Elements.full
-    ) : List[(Path, XML.Body)] = {
+    ) : List[(Command.Blob, XML.Body)] = {
       snippet_command match {
         case None => Nil
         case Some(command) =>
@@ -605,7 +605,7 @@
                 markup.to_XML(Text.Range(0, text.length), text, elements)
               }
               else Nil
-            blob.src_path -> xml
+            blob -> xml
           }
       }
     }
diff -r 540aad9405b1 -r 4da80799352f src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Fri Aug 19 21:04:14 2022 +0200
+++ b/src/Pure/PIDE/resources.scala	Fri Aug 19 21:25:13 2022 +0200
@@ -16,9 +16,6 @@
   def empty: Resources =
     new Resources(Sessions.Structure.empty, Sessions.Structure.empty.bootstrap)
 
-  def file_node(file: Path, dir: String = "", theory: String = ""): Document.Node.Name =
-    empty.file_node(file, dir = dir, theory = theory)
-
   def hidden_node(name: Document.Node.Name): Boolean =
     !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name)
 
diff -r 540aad9405b1 -r 4da80799352f src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Fri Aug 19 21:04:14 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Fri Aug 19 21:25:13 2022 +0200
@@ -44,12 +44,12 @@
     def theory_html(theory: Document_Info.Theory): Path =
       Path.explode(theory.print_short).html
 
-    def file_html(theory: Document_Info.Theory, file: Path): Path =
-      Path.explode(theory.print_short) + file.squash.html
+    def file_html(theory: Document_Info.Theory, file: String): Path =
+      Path.explode(theory.print_short) + Path.explode(file).squash.html
 
-    def smart_html(theory: Document_Info.Theory, file: Path): Path =
-      if (File.is_thy(file.file_name)) theory_html(theory)
-      else file_html(theory, file: Path)
+    def smart_html(theory: Document_Info.Theory, file: String): Path =
+      if (File.is_thy(file)) theory_html(theory)
+      else file_html(theory, file)
 
     def relative_link(dir: Path, file: Path): String =
       try { File.path(dir.java_path.relativize(file.java_path).toFile).implode }
@@ -192,7 +192,7 @@
                 html_ref <- logical_ref(theory) orElse physical_ref(theory)
               }
               yield {
-                val html_path = session_dir + html_context.smart_html(theory, Path.explode(def_file))
+                val html_path = session_dir + html_context.smart_html(theory, def_file)
                 val html_link = html_context.relative_link(file_dir, html_path)
                 HTML.entity_ref(HTML.link(html_link + "#" + html_ref, body))
               }
@@ -507,25 +507,25 @@
             make_html(Entity_Context.make(html_context, session_name, theory_name, theory.thy_file),
               thy_elements, snapshot.xml_markup(elements = thy_elements.html)))
 
-        val files_html =
+        val blobs_html =
           for {
-            (src_path, xml) <- snapshot.xml_markup_blobs(elements = thy_elements.html)
+            (blob, xml) <- snapshot.xml_markup_blobs(elements = thy_elements.html)
             if xml.nonEmpty
           }
           yield {
             progress.expose_interrupt()
-            if (verbose) progress.echo("Presenting file " + src_path)
-            (src_path, html_context.source(make_html(Entity_Context.empty, thy_elements, xml)))
+            if (verbose) progress.echo("Presenting file " + quote(blob.name.node))
+            (blob, html_context.source(make_html(Entity_Context.empty, thy_elements, xml)))
           }
 
         val files =
           for {
-            (src_path, file_html) <- files_html
-            file_path = session_dir + html_context.file_html(theory, src_path)
+            (blob, file_html) <- blobs_html
+            file_path = session_dir + html_context.file_html(theory, blob.name.node)
             rel_path <- File.relative_path(session_dir, file_path)
           }
           yield {
-            val file_title = "File " + Symbol.cartouche_decoded(src_path.implode_short)
+            val file_title = "File " + Symbol.cartouche_decoded(blob.src_path.implode_short)
             HTML.write_document(file_path.dir, file_path.file_name,
               List(HTML.title(file_title)), List(html_context.head(file_title), file_html),
               base = Some(html_context.root_dir))
diff -r 540aad9405b1 -r 4da80799352f src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Fri Aug 19 21:04:14 2022 +0200
+++ b/src/Pure/Tools/build_job.scala	Fri Aug 19 21:25:13 2022 +0200
@@ -29,7 +29,13 @@
       (thy_file, blobs_files) <- theory_context.files(permissive = true)
     }
     yield {
-      val node_name = Resources.file_node(Path.explode(thy_file), theory = theory_context.theory)
+      val master_dir =
+        Thy_Header.split_file_name(thy_file) match {
+          case Some((dir, _)) => dir
+          case None => 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 results =
         Command.Results.make(
@@ -38,8 +44,8 @@
 
       val blobs =
         blobs_files.map { file =>
+          val name = Document.Node.Name(file)
           val path = Path.explode(file)
-          val name = Resources.file_node(path)
           val src_path = File.relative_path(node_name.master_dir_path, path).getOrElse(path)
           Command.Blob(name, src_path, None)
         }