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 =