src/Pure/Tools/build_job.scala

   {
     def read(name: String): Export.Entry =
       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 {
       case (Value.Long(id), thy_file :: blobs_files) =>
         val node_name = resources.file_node(Path.explode(thy_file), theory = theory)

         else Nil
 
       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 =
           {
             result_base.load_commands.get(name.expand) match {
               case Some(spans) =>

           catch { case _: IllegalStateException => }
         }
       }
 
       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)
       val command_timings = new mutable.ListBuffer[Properties.T]
       val theory_timings = new mutable.ListBuffer[Properties.T]