# HG changeset patch
# User wenzelm
# Date 1671802373 -3600
# Node ID 0d08ee0c1ea0ae39cf01d303311b2f36e56e3654
# Parent  907b5c4d13321a1cac6d6435d3f4ad4731cbc162
clarified signature: more explicit types;

diff -r 907b5c4d1332 -r 0d08ee0c1ea0 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Fri Dec 23 12:14:10 2022 +0100
+++ b/src/Pure/Thy/document_build.scala	Fri Dec 23 14:32:53 2022 +0100
@@ -132,6 +132,13 @@
     List("isabelle.sty", "isabellesym.sty", "pdfsetup.sty", "railsetup.sty").
       map(name => texinputs + Path.basic(name))
 
+  sealed case class Document_Latex(name: Document.Node.Name, body: XML.Body) {
+    def content: File.Content_XML = File.content(Path.basic(tex_name(name)), body)
+    def file_pos: String = name.path.implode_symbolic
+    def write(latex_output: Latex.Output, dir: Path): Unit =
+      content.output(latex_output(_, file_pos = file_pos)).write(dir)
+  }
+
   def context(
     session_context: Export.Session_Context,
     document_session: Option[Sessions.Base] = None,
@@ -185,18 +192,16 @@
     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, String)] =
+    lazy val document_latex: List[Document_Latex] =
       for (name <- all_document_theories)
       yield {
-        val path = Path.basic(tex_name(name))
-        val content =
+        val body =
           if (document_selection(name)) {
             val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true)
             YXML.parse_body(entry.text)
           }
           else Nil
-        val file_pos = name.path.implode_symbolic
-        (File.content(path, content), file_pos)
+        Document_Latex(name, body)
       }
 
     lazy val session_graph: File.Content = {
@@ -263,11 +268,7 @@
       }
 
       session_tex.write(doc_dir)
-
-      for ((content, file_pos) <- document_latex) {
-        content.output(latex_output(_, file_pos = file_pos))
-          .write(doc_dir)
-      }
+      document_latex.foreach(_.write(latex_output, doc_dir))
 
       val root_name1 = "root_" + doc.name
       val root_name = if ((doc_dir + Path.explode(root_name1).tex).is_file) root_name1 else "root"