--- a/src/HOL/Tools/Mirabelle/mirabelle.scala Tue Jun 11 11:07:48 2024 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Tue Jun 11 14:18:19 2024 +0200
@@ -72,7 +72,7 @@
progress.echo(
"Mirabelle export " + quote(args.compound_name) + " (in " + session_name + ")",
verbose = true)
- val yxml = YXML.parse_body(UTF8.decode_permissive(msg.chunk), cache = build_results0.cache)
+ val yxml = YXML.parse_body(msg.chunk.text, cache = build_results0.cache)
val lines = Pretty.string_of(yxml).trim()
val prefix =
Export.explode_name(args.name) match {