diff -r 25f5f1fa31bb -r 161e84e6b40a src/Pure/PIDE/xml.scala --- a/src/Pure/PIDE/xml.scala Mon Nov 08 09:31:26 2021 +0000 +++ b/src/Pure/PIDE/xml.scala Mon Nov 08 12:45:35 2021 +0100 @@ -199,15 +199,15 @@ object Cache { def make( - xz: XZ.Cache = XZ.Cache.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(xz, max_string, initial_size) val none: Cache = make(XZ.Cache.none, max_string = 0) } - class Cache private[XML](val xz: XZ.Cache, max_string: Int, initial_size: Int) + class Cache(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 =