| author | paulson | 
| Mon, 08 Nov 2021 09:31:26 +0000 | |
| changeset 74730 | 25f5f1fa31bb | 
| parent 73024 | 337e1b135d2f | 
| child 75393 | 87ebf5a50283 | 
| permissions | -rw-r--r-- | 
| 64000 | 1 | /* Title: Pure/General/xz.scala | 
| 52671 
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
 wenzelm parents: diff
changeset | 2 | Author: Makarius | 
| 
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
 wenzelm parents: diff
changeset | 3 | |
| 64002 | 4 | Support for XZ data compression. | 
| 52671 
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
 wenzelm parents: diff
changeset | 5 | */ | 
| 
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
 wenzelm parents: diff
changeset | 6 | |
| 
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
 wenzelm parents: diff
changeset | 7 | package isabelle | 
| 
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
 wenzelm parents: diff
changeset | 8 | |
| 
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
 wenzelm parents: diff
changeset | 9 | |
| 68018 | 10 | import org.tukaani.xz.{LZMA2Options, ArrayCache, BasicArrayCache}
 | 
| 52671 
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
 wenzelm parents: diff
changeset | 11 | |
| 
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
 wenzelm parents: diff
changeset | 12 | |
| 64000 | 13 | object XZ | 
| 52671 
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
 wenzelm parents: diff
changeset | 14 | {
 | 
| 68018 | 15 | /* options */ | 
| 16 | ||
| 64002 | 17 | type Options = LZMA2Options | 
| 18 | ||
| 64004 | 19 | def options(preset: Int = 3): Options = | 
| 64000 | 20 |   {
 | 
| 21 | val opts = new LZMA2Options | |
| 22 | opts.setPreset(preset) | |
| 23 | opts | |
| 24 | } | |
| 68018 | 25 | |
| 26 | ||
| 27 | /* cache */ | |
| 28 | ||
| 29 | type Cache = ArrayCache | |
| 30 | ||
| 73024 | 31 | object Cache | 
| 32 |   {
 | |
| 33 | def none: ArrayCache = ArrayCache.getDummyCache() | |
| 34 | def apply(): ArrayCache = ArrayCache.getDefaultCache() | |
| 35 | def make(): ArrayCache = new BasicArrayCache | |
| 36 | } | |
| 52671 
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
 wenzelm parents: diff
changeset | 37 | } |