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 =