src/Pure/Thy/export.scala

     msg + " " + quote(name) + " for theory " + quote(theory_name)
 
   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,
     theory_name: String,
     name: String,
     executable: Boolean,
     body: Future[(Boolean, Bytes)],
-    cache: XZ.Cache)
+    cache: XML.Cache)
   {
     override def toString: String = name
 
     def compound_name: String = Export.compound_name(theory_name, name)
 

     def text: String = uncompressed.text
 
     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 =
       YXML.parse_body(UTF8.decode_permissive(uncompressed))
 

     (theory_name: String, name: String) =>
       regex.pattern.matcher(compound_name(theory_name, name)).matches
   }
 
   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 =
       Data.table.select(List(Data.executable, Data.compressed, Data.body),
         Data.where_equal(session_name, theory_name, name))

       }
       else None
     })
   }
 
-  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)
     if (path.is_file) {
       val executable = File.is_executable(path)

   }
 
 
   /* database consumer thread */
 
-  def consumer(db: SQL.Database, cache: XZ.Cache): Consumer = new Consumer(db, cache)
-
-  class Consumer private[Export](db: SQL.Database, cache: XZ.Cache)
+  def consumer(db: SQL.Database, cache: XML.Cache): Consumer = new Consumer(db, cache)
+
+  class Consumer private[Export](db: SQL.Database, cache: XML.Cache)
   {
     private val errors = Synchronized[List[String]](Nil)
 
     private val consumer =
       Consumer_Thread.fork_bulk[(Entry, Boolean)](name = "export")(

         def focus(other_theory: String): Provider = this
 
         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)
 
         def focus(other_theory: String): Provider =
           if (other_theory == theory_name) this
           else Provider.database(db, cache, session_name, other_theory)
 
         override def toString: String = db.toString
       }
+    }
 
     def snapshot(snapshot: Document.Snapshot): Provider =
       new Provider {
         def apply(export_name: String): Option[Entry] =
           snapshot.exports_map.get(export_name)

           }
 
         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)
 
         def focus(other_theory: String): Provider =
           if (other_theory == theory_name) this
           else Provider.directory(dir, cache, session_name, other_theory)
 
         override def toString: String = dir.toString
       }
+    }
   }
 
   trait Provider
   {
     def apply(export_name: String): Option[Entry]

               (theory_name, name) <- export_names if matcher(theory_name, name)
             } yield (theory_name, name)).toSet
           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 =
               if (elems.length < export_prune + 1) {
                 error("Cannot prune path by " + export_prune + " element(s): " + Path.make(elems))