src/Pure/General/xz.scala
changeset 71961 af779738a8f9
parent 68018 3747fe57eb67
child 73024 337e1b135d2f
equal deleted inserted replaced
71960:6a64205b491a 71961:af779738a8f9
    26 
    26 
    27   /* cache */
    27   /* cache */
    28 
    28 
    29   type Cache = ArrayCache
    29   type Cache = ArrayCache
    30 
    30 
       
    31   def no_cache(): ArrayCache = ArrayCache.getDummyCache()
    31   def cache(): ArrayCache = ArrayCache.getDefaultCache()
    32   def cache(): ArrayCache = ArrayCache.getDefaultCache()
    32   def make_cache(): ArrayCache = new BasicArrayCache
    33   def make_cache(): ArrayCache = new BasicArrayCache
    33 }
    34 }