src/Pure/Thy/document_build.scala
changeset 75824 a2b2e8964e1a
parent 75822 0a14663dffcc
child 75825 ad00fbf64bff
--- 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)
         })
     }