# HG changeset patch
# User wenzelm
# Date 1609622554 -3600
# Node ID f93f0597f4fb2d4ff35962de90d1499c65d3e783
# Parent  72a8fdfa185d5db6c4666309f671ee2dd4182c1a
clarified signature: absorb XZ.Cache into XML.Cache;

diff -r 72a8fdfa185d -r f93f0597f4fb src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/Admin/build_log.scala	Sat Jan 02 22:22:34 2021 +0100
@@ -244,10 +244,10 @@
 
     /* properties (YXML) */
 
-    val xml_cache: XML.Cache = XML.Cache.make()
+    val cache: XML.Cache = XML.Cache.make()
 
     def parse_props(text: String): Properties.T =
-      try { xml_cache.props(XML.Decode.properties(YXML.parse_body(text))) }
+      try { cache.props(XML.Decode.properties(YXML.parse_body(text))) }
       catch { case _: XML.Error => log_file.err("malformed properties") }
 
     def filter_props(marker: Protocol_Message.Marker): List[Properties.T] =
@@ -850,15 +850,10 @@
 
   /* database access */
 
-  def store(options: Options,
-      xml_cache: XML.Cache = XML.Cache.make(),
-      xz_cache: XZ.Cache = XZ.Cache.make()): Store =
-    new Store(options, xml_cache, xz_cache)
+  def store(options: Options, cache: XML.Cache = XML.Cache.make()): Store =
+    new Store(options, cache)
 
-  class Store private[Build_Log](
-    options: Options,
-    val xml_cache: XML.Cache,
-    val xz_cache: XZ.Cache)
+  class Store private[Build_Log](options: Options, val cache: XML.Cache)
   {
     def open_database(
       user: String = options.string("build_log_database_user"),
@@ -996,7 +991,7 @@
           stmt.double(13) = session.ml_timing.factor
           stmt.long(14) = session.heap_size
           stmt.string(15) = session.status.map(_.toString)
-          stmt.bytes(16) = compress_errors(session.errors, cache = xz_cache)
+          stmt.bytes(16) = compress_errors(session.errors, cache = cache.xz)
           stmt.string(17) = session.sources
           stmt.execute()
         }
@@ -1034,7 +1029,7 @@
       {
         val ml_stats: List[(String, Option[Bytes])] =
           Par_List.map[(String, Session_Entry), (String, Option[Bytes])](
-            { case (a, b) => (a, Properties.compress(b.ml_statistics, cache = xz_cache).proper) },
+            { case (a, b) => (a, Properties.compress(b.ml_statistics, cache = cache.xz).proper) },
             build_info.sessions.iterator.filter(p => p._2.ml_statistics.nonEmpty).toList)
         val entries = if (ml_stats.nonEmpty) ml_stats else List("" -> None)
         for ((session_name, ml_statistics) <- entries) {
@@ -1163,11 +1158,10 @@
                 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 = xz_cache),
+                errors = uncompress_errors(res.bytes(Data.errors), cache = cache.xz),
                 ml_statistics =
                   if (ml_statistics) {
-                    Properties.uncompress(
-                      res.bytes(Data.ml_statistics), cache = xz_cache, xml_cache = xml_cache)
+                    Properties.uncompress(res.bytes(Data.ml_statistics), cache = cache)
                   }
                   else Nil)
             session_name -> session_entry
diff -r 72a8fdfa185d -r f93f0597f4fb src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/Admin/build_status.scala	Sat Jan 02 22:22:34 2021 +0100
@@ -286,8 +286,7 @@
             val ml_stats =
               ML_Statistics(
                 if (ml_statistics) {
-                  Properties.uncompress(
-                    res.bytes(Build_Log.Data.ml_statistics), cache = store.xz_cache)
+                  Properties.uncompress(res.bytes(Build_Log.Data.ml_statistics), cache = store.cache)
                 }
                 else Nil,
                 domain = ml_statistics_domain,
@@ -320,8 +319,8 @@
                 stored_heap = ML_Statistics.mem_scale(res.long(Build_Log.Data.heap_size)),
                 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.xz_cache))
+                  Build_Log.uncompress_errors(
+                    res.bytes(Build_Log.Data.errors), cache = store.cache.xz))
 
             val sessions = data_entries.getOrElse(data_name, Map.empty)
             val session =
diff -r 72a8fdfa185d -r f93f0597f4fb src/Pure/General/cache.scala
--- a/src/Pure/General/cache.scala	Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/General/cache.scala	Sat Jan 02 22:22:34 2021 +0100
@@ -16,7 +16,9 @@
   val default_max_string = 100
   val default_initial_size = 131071
 
-  def make(max_string: Int = default_max_string, initial_size: Int = default_initial_size): Cache =
+  def make(
+      max_string: Int = default_max_string,
+      initial_size: Int = default_initial_size): Cache =
     new Cache(max_string, initial_size)
 
   val none: Cache = make(max_string = 0)
diff -r 72a8fdfa185d -r f93f0597f4fb src/Pure/General/properties.scala
--- a/src/Pure/General/properties.scala	Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/General/properties.scala	Sat Jan 02 22:22:34 2021 +0100
@@ -37,8 +37,8 @@
 
   def encode(ps: T): Bytes = Bytes(YXML.string_of_body(XML.Encode.properties(ps)))
 
-  def decode(bs: Bytes, xml_cache: XML.Cache = XML.Cache.none): T =
-    xml_cache.props(XML.Decode.properties(YXML.parse_body(bs.text)))
+  def decode(bs: Bytes, cache: XML.Cache = XML.Cache.none): T =
+    cache.props(XML.Decode.properties(YXML.parse_body(bs.text)))
 
   def compress(ps: List[T],
     options: XZ.Options = XZ.options(),
@@ -51,15 +51,14 @@
     }
   }
 
-  def uncompress(bs: Bytes,
-    cache: XZ.Cache = XZ.Cache(),
-    xml_cache: XML.Cache = XML.Cache.none): List[T] =
+  def uncompress(bs: Bytes, cache: XML.Cache = XML.Cache.none): List[T] =
   {
     if (bs.is_empty) Nil
     else {
       val ps =
-        XML.Decode.list(XML.Decode.properties)(YXML.parse_body(bs.uncompress(cache = cache).text))
-      if (xml_cache.no_cache) ps else ps.map(xml_cache.props)
+        XML.Decode.list(XML.Decode.properties)(
+          YXML.parse_body(bs.uncompress(cache = cache.xz).text))
+      if (cache.no_cache) ps else ps.map(cache.props)
     }
   }
 
diff -r 72a8fdfa185d -r f93f0597f4fb src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Sat Jan 02 22:22:34 2021 +0100
@@ -99,7 +99,7 @@
     private def consume(props: Properties.T): Unit = synchronized
     {
       if (session != null) {
-        val props1 = (session.xml_cache.props(props ::: Java_Statistics.jvm_statistics()))
+        val props1 = (session.cache.props(props ::: Java_Statistics.jvm_statistics()))
         session.runtime_statistics.post(Session.Runtime_Statistics(props1))
       }
     }
diff -r 72a8fdfa185d -r f93f0597f4fb src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/PIDE/command.scala	Sat Jan 02 22:22:34 2021 +0100
@@ -290,7 +290,7 @@
         other_id: (Document.Node.Name, Document_ID.Generic) =>
           Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)],
         message: XML.Elem,
-        xml_cache: XML.Cache): State =
+        cache: XML.Cache): State =
       message match {
         case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
           if (command.span.is_theory) this
@@ -329,7 +329,7 @@
                           target_chunk.incorporate(symbol_range) match {
                             case Some(range) =>
                               val props = atts.filterNot(Markup.position_property)
-                              val elem = xml_cache.elem(XML.Elem(Markup(name, props), args))
+                              val elem = cache.elem(XML.Elem(Markup(name, props), args))
                               state.add_markup(false, target_name, Text.Info(range, elem))
                             case None => bad(); state
                           }
@@ -348,9 +348,9 @@
           props match {
             case Markup.Serial(i) =>
               val markup_message =
-                xml_cache.elem(XML.Elem(Markup(Markup.message(name), props), body))
+                cache.elem(XML.Elem(Markup(Markup.message(name), props), body))
               val message_markup =
-                xml_cache.elem(XML.elem(Markup(name, props.filter(p => p._1 == Markup.SERIAL))))
+                cache.elem(XML.elem(Markup(name, props.filter(p => p._1 == Markup.SERIAL))))
 
               var st = add_result(i -> markup_message)
               if (Protocol.is_inlined(message)) {
diff -r 72a8fdfa185d -r f93f0597f4fb src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Jan 02 22:22:34 2021 +0100
@@ -931,12 +931,12 @@
       (commands_redirection /: st.markups.redirection_iterator)({ case (graph, id) =>
         graph.default_node(id, ()).default_node(st.command.id, ()).add_edge(id, st.command.id) })
 
-    def accumulate(id: Document_ID.Generic, message: XML.Elem, xml_cache: XML.Cache)
+    def accumulate(id: Document_ID.Generic, message: XML.Elem, cache: XML.Cache)
       : (Command.State, State) =
     {
       def update(st: Command.State): (Command.State, State) =
       {
-        val st1 = st.accumulate(self_id(st), other_id, message, xml_cache)
+        val st1 = st.accumulate(self_id(st), other_id, message, cache)
         (st1, copy(commands_redirection = redirection(st1)))
       }
       execs.get(id).map(update) match {
diff -r 72a8fdfa185d -r f93f0597f4fb src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/PIDE/prover.scala	Sat Jan 02 22:22:34 2021 +0100
@@ -64,7 +64,7 @@
 
 class Prover(
   receiver: Prover.Receiver,
-  xml_cache: XML.Cache,
+  cache: XML.Cache,
   channel: System_Channel,
   process: Bash.Process) extends Protocol
 {
@@ -77,14 +77,14 @@
 
   private def protocol_output(props: Properties.T, bytes: Bytes)
   {
-    receiver(new Prover.Protocol_Output(xml_cache.props(props), bytes))
+    receiver(new Prover.Protocol_Output(cache.props(props), bytes))
   }
 
   private def output(kind: String, props: Properties.T, body: XML.Body)
   {
     val main = XML.Elem(Markup(kind, props), Protocol_Message.clean_reports(body))
     val reports = Protocol_Message.reports(props, body)
-    for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg)))
+    for (msg <- main :: reports) receiver(new Prover.Output(cache.elem(msg)))
   }
 
   private def exit_message(result: Process_Result)
diff -r 72a8fdfa185d -r f93f0597f4fb src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/PIDE/session.scala	Sat Jan 02 22:22:34 2021 +0100
@@ -127,8 +127,7 @@
 {
   session =>
 
-  val xml_cache: XML.Cache = XML.Cache.make()
-  val xz_cache: XZ.Cache = XZ.Cache.make()
+  val cache: XML.Cache = XML.Cache.make()
 
   def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info =
     Command.Blobs_Info.none
@@ -496,7 +495,7 @@
               case Protocol.Command_Timing(props, state_id, timing) if prover.defined =>
                 command_timings.post(Session.Command_Timing(props))
                 val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
-                change_command(_.accumulate(state_id, xml_cache.elem(message), xml_cache))
+                change_command(_.accumulate(state_id, cache.elem(message), cache))
 
               case Markup.Theory_Timing(props) =>
                 theory_timings.post(Session.Theory_Timing(props))
@@ -507,7 +506,7 @@
               case Protocol.Export(args)
               if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
                 val id = Value.Long.unapply(args.id.get).get
-                val export = Export.make_entry("", args, msg.bytes, cache = xz_cache)
+                val export = Export.make_entry("", args, msg.bytes, cache)
                 change_command(_.add_export(id, (args.serial, export)))
 
               case Protocol.Loading_Theory(node_name, id) =>
@@ -519,7 +518,7 @@
                 msg.text match {
                   case Protocol.Commands_Accepted(ids) =>
                     ids.foreach(id =>
-                      change_command(_.accumulate(id, Protocol.Commands_Accepted.message, xml_cache)))
+                      change_command(_.accumulate(id, Protocol.Commands_Accepted.message, cache)))
                   case _ => bad_output()
                 }
 
@@ -554,7 +553,7 @@
         case _ =>
           output.properties match {
             case Position.Id(state_id) =>
-              change_command(_.accumulate(state_id, output.message, xml_cache))
+              change_command(_.accumulate(state_id, output.message, cache))
 
             case _ if output.is_init =>
               val init_ok =
diff -r 72a8fdfa185d -r f93f0597f4fb src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/PIDE/xml.scala	Sat Jan 02 22:22:34 2021 +0100
@@ -174,14 +174,15 @@
   object Cache
   {
     def make(
-        max_string: Int = isabelle.Cache.default_max_string,
+      xz: XZ.Cache = XZ.Cache.make(),
+      max_string: Int = isabelle.Cache.default_max_string,
         initial_size: Int = isabelle.Cache.default_initial_size): Cache =
-      new Cache(max_string, initial_size)
+      new Cache(xz, max_string, initial_size)
 
-    val none: Cache = make(max_string = 0)
+    val none: Cache = make(XZ.Cache.none, max_string = 0)
   }
 
-  class Cache private[XML](max_string: Int, initial_size: Int)
+  class Cache private[XML](val xz: XZ.Cache, max_string: Int, initial_size: Int)
     extends isabelle.Cache(max_string, initial_size)
   {
     protected def cache_props(x: Properties.T): Properties.T =
diff -r 72a8fdfa185d -r f93f0597f4fb src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/System/isabelle_process.scala	Sat Jan 02 22:22:34 2021 +0100
@@ -62,7 +62,7 @@
       case _ =>
     }
 
-  session.start(receiver => new Prover(receiver, session.xml_cache, channel, process))
+  session.start(receiver => new Prover(receiver, session.cache, channel, process))
 
   def await_startup(): Isabelle_Process =
     startup.join match {
diff -r 72a8fdfa185d -r f93f0597f4fb src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/Thy/export.scala	Sat Jan 02 22:22:34 2021 +0100
@@ -85,7 +85,7 @@
   def compound_name(a: String, b: String): String = a + ":" + b
 
   def empty_entry(theory_name: String, name: String): Entry =
-    Entry("", theory_name, name, false, Future.value(false, Bytes.empty), XZ.Cache.none)
+    Entry("", theory_name, name, false, Future.value(false, Bytes.empty), XML.Cache.none)
 
   sealed case class Entry(
     session_name: String,
@@ -93,7 +93,7 @@
     name: String,
     executable: Boolean,
     body: Future[(Boolean, Bytes)],
-    cache: XZ.Cache)
+    cache: XML.Cache)
   {
     override def toString: String = name
 
@@ -110,7 +110,7 @@
     def uncompressed: Bytes =
     {
       val (compressed, bytes) = body.join
-      if (compressed) bytes.uncompress(cache = cache) else bytes
+      if (compressed) bytes.uncompress(cache = cache.xz) else bytes
     }
 
     def uncompressed_yxml: XML.Body =
@@ -158,17 +158,15 @@
   }
 
   def make_entry(
-    session_name: String, args: Protocol.Export.Args, bytes: Bytes,
-    cache: XZ.Cache): Entry =
+    session_name: String, args: Protocol.Export.Args, bytes: Bytes, cache: XML.Cache): Entry =
   {
     val body =
-      if (args.compress) Future.fork(bytes.maybe_compress(cache = cache))
+      if (args.compress) Future.fork(bytes.maybe_compress(cache = cache.xz))
       else Future.value((false, bytes))
     Entry(session_name, args.theory_name, args.name, args.executable, body, cache)
   }
 
-  def read_entry(
-    db: SQL.Database, cache: XZ.Cache,
+  def read_entry(db: SQL.Database, cache: XML.Cache,
     session_name: String, theory_name: String, name: String): Option[Entry] =
   {
     val select =
@@ -188,8 +186,7 @@
     })
   }
 
-  def read_entry(
-    dir: Path, cache: XZ.Cache,
+  def read_entry(dir: Path, cache: XML.Cache,
     session_name: String, theory_name: String, name: String): Option[Entry] =
   {
     val path = dir + Path.basic(theory_name) + Path.explode(name)
@@ -205,9 +202,9 @@
 
   /* database consumer thread */
 
-  def consumer(db: SQL.Database, cache: XZ.Cache): Consumer = new Consumer(db, cache)
+  def consumer(db: SQL.Database, cache: XML.Cache): Consumer = new Consumer(db, cache)
 
-  class Consumer private[Export](db: SQL.Database, cache: XZ.Cache)
+  class Consumer private[Export](db: SQL.Database, cache: XML.Cache)
   {
     private val errors = Synchronized[List[String]](Nil)
 
@@ -271,9 +268,9 @@
         override def toString: String = context.toString
       }
 
-    def database(
-        db: SQL.Database, cache: XZ.Cache,
-        session_name: String, theory_name: String): Provider =
+    def database(db: SQL.Database, cache: XML.Cache, session_name: String, theory_name: String)
+      : Provider =
+    {
       new Provider {
         def apply(export_name: String): Option[Entry] =
           read_entry(db, cache, session_name, theory_name, export_name)
@@ -284,6 +281,7 @@
 
         override def toString: String = db.toString
       }
+    }
 
     def snapshot(snapshot: Document.Snapshot): Provider =
       new Provider {
@@ -302,9 +300,9 @@
         override def toString: String = snapshot.toString
       }
 
-    def directory(
-        dir: Path, cache: XZ.Cache,
-        session_name: String, theory_name: String): Provider =
+    def directory(dir: Path, cache: XML.Cache, session_name: String, theory_name: String)
+      : Provider =
+    {
       new Provider {
         def apply(export_name: String): Option[Entry] =
           read_entry(dir, cache, session_name, theory_name, export_name)
@@ -315,6 +313,7 @@
 
         override def toString: String = dir.toString
       }
+    }
   }
 
   trait Provider
@@ -364,7 +363,7 @@
           for {
             (theory_name, group) <- exports.toList.groupBy(_._1).toList.sortBy(_._1)
             name <- group.map(_._2).sorted
-            entry <- read_entry(db, store.xz_cache, session_name, theory_name, name)
+            entry <- read_entry(db, store.cache, session_name, theory_name, name)
           } {
             val elems = theory_name :: space_explode('/', name)
             val path =
diff -r 72a8fdfa185d -r f93f0597f4fb src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/Thy/export_theory.scala	Sat Jan 02 22:22:34 2021 +0100
@@ -41,8 +41,8 @@
             for (theory <- Export.read_theory_names(db, session))
             yield {
               progress.echo("Reading theory " + theory)
-              read_theory(Export.Provider.database(db, store.xz_cache, session, theory),
-                session, theory, cache = cache)
+              val provider = Export.Provider.database(db, store.cache, session, theory)
+              read_theory(provider, session, theory, cache = cache)
             }
           }
         }))
@@ -145,8 +145,8 @@
     using(store.open_database(session_name))(db =>
     {
       db.transaction {
-        read(Export.Provider.database(
-          db, store.xz_cache, session_name, theory_name), session_name, theory_name)
+        val provider = Export.Provider.database(db, store.cache, session_name, theory_name)
+        read(provider, session_name, theory_name)
       }
     })
   }
diff -r 72a8fdfa185d -r f93f0597f4fb src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/Thy/sessions.scala	Sat Jan 02 22:22:34 2021 +0100
@@ -1203,8 +1203,7 @@
     val store: Sessions.Store,
     database_server: Option[SQL.Database]) extends AutoCloseable
   {
-    def xml_cache: XML.Cache = store.xml_cache
-    def xz_cache: XZ.Cache = store.xz_cache
+    def cache: XML.Cache = store.cache
 
     def close { database_server.foreach(_.close) }
 
@@ -1231,12 +1230,12 @@
         database_server match {
           case Some(db) =>
             sessions.view.map(session_name =>
-              Export.read_entry(db, store.xz_cache, session_name, theory_name, name))
+              Export.read_entry(db, store.cache, session_name, theory_name, name))
           case None =>
             sessions.view.map(session_name =>
               store.try_open_database(session_name) match {
                 case Some(db) =>
-                  using(db)(Export.read_entry(_, store.xz_cache, session_name, theory_name, name))
+                  using(db)(Export.read_entry(_, store.cache, session_name, theory_name, name))
                 case None => None
               })
         }
@@ -1259,15 +1258,10 @@
     }
   }
 
-  def store(options: Options,
-      xml_cache: XML.Cache = XML.Cache.make(),
-      xz_cache: XZ.Cache = XZ.Cache.make()): Store =
-    new Store(options, xml_cache, xz_cache)
+  def store(options: Options, cache: XML.Cache = XML.Cache.make()): Store =
+    new Store(options, cache)
 
-  class Store private[Sessions](
-    val options: Options,
-    val xml_cache: XML.Cache,
-    val xz_cache: XZ.Cache)
+  class Store private[Sessions](val options: Options, val cache: XML.Cache)
   {
     store =>
 
@@ -1407,8 +1401,7 @@
       })
 
     def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] =
-      Properties.uncompress(
-        read_bytes(db, name, column), cache = xz_cache, xml_cache = xml_cache)
+      Properties.uncompress(read_bytes(db, name, column), cache = cache)
 
 
     /* session info */
@@ -1459,11 +1452,11 @@
         {
           stmt.string(1) = name
           stmt.bytes(2) = Properties.encode(build_log.session_timing)
-          stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = xz_cache)
-          stmt.bytes(4) = Properties.compress(build_log.theory_timings, cache = xz_cache)
-          stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = xz_cache)
-          stmt.bytes(6) = Properties.compress(build_log.task_statistics, cache = xz_cache)
-          stmt.bytes(7) = Build_Log.compress_errors(build_log.errors, cache = xz_cache)
+          stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = cache.xz)
+          stmt.bytes(4) = Properties.compress(build_log.theory_timings, cache = cache.xz)
+          stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = cache.xz)
+          stmt.bytes(6) = Properties.compress(build_log.task_statistics, cache = cache.xz)
+          stmt.bytes(7) = Build_Log.compress_errors(build_log.errors, cache = cache.xz)
           stmt.string(8) = build.sources
           stmt.string(9) = cat_lines(build.input_heaps)
           stmt.string(10) = build.output_heap getOrElse ""
@@ -1474,7 +1467,7 @@
     }
 
     def read_session_timing(db: SQL.Database, name: String): Properties.T =
-      Properties.decode(read_bytes(db, name, Session_Info.session_timing), xml_cache = xml_cache)
+      Properties.decode(read_bytes(db, name, Session_Info.session_timing), cache = cache)
 
     def read_command_timings(db: SQL.Database, name: String): List[Properties.T] =
       read_properties(db, name, Session_Info.command_timings)
@@ -1492,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 = xz_cache)
+      Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors), cache = cache.xz)
 
     def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
     {
diff -r 72a8fdfa185d -r f93f0597f4fb src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/Tools/build_job.scala	Sat Jan 02 22:22:34 2021 +0100
@@ -25,7 +25,7 @@
       db_context.get_export(List(session), theory, name)
 
     def read_xml(name: String): XML.Body =
-      db_context.xml_cache.body(YXML.parse_body(
+      db_context.cache.body(YXML.parse_body(
         Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).uncompressed))))
 
     (read(Export.DOCUMENT_ID).text, split_lines(read(Export.FILES).text)) match {
@@ -234,8 +234,7 @@
       val resources = new Resources(sessions_structure, base, command_timings = command_timings0)
       val session =
         new Session(options, resources) {
-          override val xml_cache: XML.Cache = store.xml_cache
-          override val xz_cache: XZ.Cache = store.xz_cache
+          override val cache: XML.Cache = store.cache
 
           override def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info =
           {
@@ -262,7 +261,7 @@
       }
 
       val export_consumer =
-        Export.consumer(store.open_database(session_name, output = true), store.xz_cache)
+        Export.consumer(store.open_database(session_name, output = true), store.cache)
 
       val stdout = new StringBuilder(1000)
       val stderr = new StringBuilder(1000)
diff -r 72a8fdfa185d -r f93f0597f4fb src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/Tools/debugger.scala	Sat Jan 02 22:22:34 2021 +0100
@@ -133,7 +133,7 @@
           Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.bytes)) match {
             case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
               val message = XML.Elem(Markup(Markup.message(name), props), body)
-              debugger.add_output(thread_name, i -> session.xml_cache.elem(message))
+              debugger.add_output(thread_name, i -> session.cache.elem(message))
               true
             case _ => false
           }
diff -r 72a8fdfa185d -r f93f0597f4fb src/Pure/term.scala
--- a/src/Pure/term.scala	Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/term.scala	Sat Jan 02 22:22:34 2021 +0100
@@ -144,7 +144,7 @@
   }
 
   class Cache private[Term](max_string: Int, initial_size: Int)
-    extends isabelle.Cache(max_string = max_string, initial_size = initial_size)
+    extends isabelle.Cache(max_string, initial_size)
   {
     protected def cache_indexname(x: Indexname): Indexname =
       lookup(x) getOrElse store(Indexname(cache_string(x.name), x.index))