clarified caching;

--- 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)

--- a/src/Pure/Admin/build_status.scala	Sat Jan 02 22:40:06 2021 +0100
+++ b/src/Pure/Admin/build_status.scala	Sat Jan 02 22:50:09 2021 +0100
@@ -320,7 +320,7 @@
                 status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status)),
                 errors =
                   Build_Log.uncompress_errors(
-                    res.bytes(Build_Log.Data.errors), cache = store.cache.xz))
+                    res.bytes(Build_Log.Data.errors), cache = store.cache))
 
             val sessions = data_entries.getOrElse(data_name, Map.empty)
             val session =

--- a/src/Pure/Thy/export.scala	Sat Jan 02 22:40:06 2021 +0100
+++ b/src/Pure/Thy/export.scala	Sat Jan 02 22:50:09 2021 +0100
@@ -114,7 +114,7 @@
     }
 
     def uncompressed_yxml: XML.Body =
-      YXML.parse_body(UTF8.decode_permissive(uncompressed))
+      YXML.parse_body(UTF8.decode_permissive(uncompressed), cache = cache)
 
     def write(db: SQL.Database)
     {

--- a/src/Pure/Thy/sessions.scala	Sat Jan 02 22:40:06 2021 +0100
+++ b/src/Pure/Thy/sessions.scala	Sat Jan 02 22:50:09 2021 +0100
@@ -1485,7 +1485,7 @@
       read_theory_timings(db, name).flatMap(Markup.Name.unapply)
 
     def read_errors(db: SQL.Database, name: String): List[String] =
-      Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors), cache = cache.xz)
+      Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors), cache = cache)
 
     def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
     {

--- a/src/Pure/Tools/build_job.scala	Sat Jan 02 22:40:06 2021 +0100
+++ b/src/Pure/Tools/build_job.scala	Sat Jan 02 22:50:09 2021 +0100
@@ -25,8 +25,9 @@
       db_context.get_export(List(session), theory, name)
 
     def read_xml(name: String): XML.Body =
-      db_context.cache.body(YXML.parse_body(
-        Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).uncompressed))))
+      YXML.parse_body(
+        Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).uncompressed)),
+        cache = db_context.cache)
 
     (read(Export.DOCUMENT_ID).text, split_lines(read(Export.FILES).text)) match {
       case (Value.Long(id), thy_file :: blobs_files) =>