changeset 73024 | 337e1b135d2f |
parent 71961 | af779738a8f9 |
child 75393 | 87ebf5a50283 |
73023:e15621aa8c72 | 73024:337e1b135d2f |
---|---|
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 object Cache |
32 def cache(): ArrayCache = ArrayCache.getDefaultCache() |
32 { |
33 def make_cache(): ArrayCache = new BasicArrayCache |
33 def none: ArrayCache = ArrayCache.getDummyCache() |
34 def apply(): ArrayCache = ArrayCache.getDefaultCache() |
|
35 def make(): ArrayCache = new BasicArrayCache |
|
36 } |
|
34 } |
37 } |