diff -r 0d08ee0c1ea0 -r 8fc7157485d8 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)