diff -r 762fcf8f9ced -r 972f7a4cdc0e src/Pure/Thy/document_build.scala --- 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 =