# HG changeset patch
# User wenzelm
# Date 1671723275 -3600
# Node ID 2afca3174629d03f7e195e7afeb3f95b284836bc
# Parent  cb72b5996520f1d468ebe9015f332c5e31e1252c
proper node name instead of not base tex_name (amending 2fd0c33fe440);

diff -r cb72b5996520 -r 2afca3174629 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Thu Dec 22 15:23:26 2022 +0100
+++ b/src/Pure/Thy/document_build.scala	Thu Dec 22 16:34:35 2022 +0100
@@ -185,7 +185,7 @@
     def session_document_theories: List[Document.Node.Name] = base.proper_session_theories
     def all_document_theories: List[Document.Node.Name] = base.all_document_theories
 
-    lazy val document_latex: List[File.Content_XML] =
+    lazy val document_latex: List[(File.Content_XML, String)] =
       for (name <- all_document_theories)
       yield {
         val path = Path.basic(tex_name(name))
@@ -195,7 +195,8 @@
             YXML.parse_body(entry.text)
           }
           else Nil
-        File.content(path, content)
+        val file_pos = name.path.implode_symbolic
+        (File.content(path, content), file_pos)
       }
 
     lazy val session_graph: File.Content = {
@@ -263,8 +264,8 @@
 
       session_tex.write(doc_dir)
 
-      for (content <- document_latex) {
-        content.output(latex_output(_, file_pos = content.path.implode_symbolic))
+      for ((content, file_pos) <- document_latex) {
+        content.output(latex_output(_, file_pos = file_pos))
           .write(doc_dir)
       }