tuned;
authorwenzelm
Fri, 23 Dec 2022 14:43:04 +0100
changeset 76758 8fc7157485d8
parent 76757 0d08ee0c1ea0
child 76759 35f41096de36
tuned;
src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Fri Dec 23 14:32:53 2022 +0100
+++ b/src/Pure/Thy/document_build.scala	Fri Dec 23 14:43:04 2022 +0100
@@ -192,17 +192,15 @@
     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[Document_Latex] =
-      for (name <- all_document_theories)
-      yield {
-        val body =
-          if (document_selection(name)) {
-            val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true)
-            YXML.parse_body(entry.text)
-          }
-          else Nil
-        Document_Latex(name, body)
-      }
+    lazy val isabelle_logo: Option[File.Content] = {
+      document_logo.map(logo_name =>
+        Isabelle_System.with_tmp_file("logo", ext = "pdf") { tmp_path =>
+          Logo.create_logo(logo_name, output_file = tmp_path, quiet = true)
+          val path = Path.basic("isabelle_logo.pdf")
+          val content = Bytes.read(tmp_path)
+          File.content(path, content)
+        })
+    }
 
     lazy val session_graph: File.Content = {
       val path = Browser_Info.session_graph_path
@@ -218,15 +216,17 @@
       File.content(path, content)
     }
 
-    lazy val isabelle_logo: Option[File.Content] = {
-      document_logo.map(logo_name =>
-        Isabelle_System.with_tmp_file("logo", ext = "pdf") { tmp_path =>
-          Logo.create_logo(logo_name, output_file = tmp_path, quiet = true)
-          val path = Path.basic("isabelle_logo.pdf")
-          val content = Bytes.read(tmp_path)
-          File.content(path, content)
-        })
-    }
+    lazy val document_latex: List[Document_Latex] =
+      for (name <- all_document_theories)
+      yield {
+        val body =
+          if (document_selection(name)) {
+            val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true)
+            YXML.parse_body(entry.text)
+          }
+          else Nil
+        Document_Latex(name, body)
+      }
 
 
     /* build document */
@@ -281,7 +281,6 @@
       /* derived material: without SHA1 digest */
 
       isabelle_logo.foreach(_.write(doc_dir))
-
       session_graph.write(doc_dir)
 
       Directory(doc_dir, doc, root_name, sources)