--- 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)
})
}