# HG changeset patch
# User wenzelm
# Date 1670849958 -3600
# Node ID 46017d6b9bfa64776d8753a6183a5968cc43cd0b
# Parent  2542ea38221545f3575fd6be491f8e97f1440748
clarified signature;

diff -r 2542ea382215 -r 46017d6b9bfa src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Mon Dec 12 13:28:18 2022 +0100
+++ b/src/Pure/Thy/document_build.scala	Mon Dec 12 13:59:18 2022 +0100
@@ -165,13 +165,11 @@
 
     def documents: List[Document_Variant] = info.documents
 
-    def proper_session_theories: List[Document.Node.Name] = base.proper_session_theories
-
-    def document_theories: List[Document.Node.Name] =
-      proper_session_theories ::: base.document_theories
+    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] =
-      for (name <- document_theories)
+      for (name <- all_document_theories)
       yield {
         val path = Path.basic(tex_name(name))
         val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true)
@@ -189,7 +187,7 @@
       val path = Path.basic("session.tex")
       val content =
         Library.terminate_lines(
-          base.proper_session_theories.map(name => "\\input{" + tex_name(name) + "}"))
+          session_document_theories.map(name => "\\input{" + tex_name(name) + "}"))
       File.content(path, content)
     }
 
diff -r 2542ea382215 -r 46017d6b9bfa src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Dec 12 13:28:18 2022 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Dec 12 13:59:18 2022 +0100
@@ -79,6 +79,9 @@
         ", loaded_theories = " + loaded_theories.size +
         ", used_theories = " + used_theories.length + ")"
 
+    def all_document_theories: List[Document.Node.Name] =
+      proper_session_theories ::: document_theories
+
     def loaded_theory(name: String): Boolean = loaded_theories.defined(name)
     def loaded_theory(name: Document.Node.Name): Boolean = loaded_theory(name.theory)