src/Pure/Thy/document_build.scala
changeset 80480 972f7a4cdc0e
parent 80236 c6670f9575de
--- a/src/Pure/Thy/document_build.scala	Tue Jul 02 22:38:00 2024 +0200
+++ b/src/Pure/Thy/document_build.scala	Tue Jul 02 23:13:35 2024 +0200
@@ -248,7 +248,7 @@
         val body =
           if (selected) {
             val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true)
-            YXML.parse_body(entry.text)
+            YXML.parse_body(entry.bytes)
           }
           else {
             val text =