--- a/src/Pure/General/xz.scala Sat Jan 02 14:24:03 2021 +0100
+++ b/src/Pure/General/xz.scala Sat Jan 02 15:58:48 2021 +0100
@@ -28,7 +28,10 @@
type Cache = ArrayCache
- def no_cache(): ArrayCache = ArrayCache.getDummyCache()
- def cache(): ArrayCache = ArrayCache.getDefaultCache()
- def make_cache(): ArrayCache = new BasicArrayCache
+ object Cache
+ {
+ def none: ArrayCache = ArrayCache.getDummyCache()
+ def apply(): ArrayCache = ArrayCache.getDefaultCache()
+ def make(): ArrayCache = new BasicArrayCache
+ }
}