src/Pure/General/xz.scala
changeset 73024 337e1b135d2f
parent 71961 af779738a8f9
child 75393 87ebf5a50283
--- 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
+  }
 }