src/Pure/Admin/build_log.scala
changeset 73033 d2690444c00a
parent 73031 f93f0597f4fb
child 73340 0ffcad1f6130
--- a/src/Pure/Admin/build_log.scala	Sat Jan 02 22:40:06 2021 +0100
+++ b/src/Pure/Admin/build_log.scala	Sat Jan 02 22:50:09 2021 +0100
@@ -655,10 +655,11 @@
         compress(cache = cache))
     }
 
-  def uncompress_errors(bytes: Bytes, cache: XZ.Cache = XZ.Cache()): List[String] =
+  def uncompress_errors(bytes: Bytes, cache: XML.Cache = XML.Cache.make()): List[String] =
     if (bytes.is_empty) Nil
     else {
-      XML.Decode.list(YXML.string_of_body)(YXML.parse_body(bytes.uncompress(cache = cache).text))
+      XML.Decode.list(YXML.string_of_body)(
+        YXML.parse_body(bytes.uncompress(cache = cache.xz).text, cache = cache))
     }
 
 
@@ -1158,7 +1159,7 @@
                 sources = res.get_string(Data.sources),
                 heap_size = res.get_long(Data.heap_size),
                 status = res.get_string(Data.status).map(Session_Status.withName),
-                errors = uncompress_errors(res.bytes(Data.errors), cache = cache.xz),
+                errors = uncompress_errors(res.bytes(Data.errors), cache = cache),
                 ml_statistics =
                   if (ml_statistics) {
                     Properties.uncompress(res.bytes(Data.ml_statistics), cache = cache)