diff -r 6eb8d6cdb686 -r a2b2e8964e1a src/Pure/Thy/document_build.scala --- a/src/Pure/Thy/document_build.scala Fri Aug 12 15:57:22 2022 +0200 +++ b/src/Pure/Thy/document_build.scala Fri Aug 12 16:01:52 2022 +0200 @@ -173,13 +173,13 @@ val path = Path.basic(tex_name(name)) val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true) val content = YXML.parse_body(entry.text) - File.Content(path, content) + File.content(path, content) } lazy val session_graph: File.Content = { val path = Presentation.session_graph_path val content = graphview.Graph_File.make_pdf(options, base.session_graph_display) - File.Content(path, content) + File.content(path, content) } lazy val session_tex: File.Content = { @@ -187,7 +187,7 @@ val content = Library.terminate_lines( base.proper_session_theories.map(name => "\\input{" + tex_name(name) + "}")) - File.Content(path, content) + File.content(path, content) } lazy val isabelle_logo: Option[File.Content] = { @@ -196,7 +196,7 @@ 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) + File.content(path, content) }) }