--- a/src/HOL/Tools/Mirabelle/mirabelle.scala Tue Jul 02 22:38:00 2024 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Tue Jul 02 23:13:35 2024 +0200
@@ -72,7 +72,7 @@
progress.echo(
"Mirabelle export " + quote(args.compound_name) + " (in " + session_name + ")",
verbose = true)
- val yxml = YXML.parse_body(msg.chunk.text, cache = build_results0.cache)
+ val yxml = YXML.parse_body(msg.chunk, cache = build_results0.cache)
val lines = Pretty.string_of(yxml).trim()
val prefix =
Export.explode_name(args.name) match {