| author | wenzelm |
| Fri, 05 Aug 2022 13:34:47 +0200 | |
| changeset 75761 | 2a0051496844 |
| parent 75620 | 44815dc2b8f9 |
| child 76350 | 978f7ca3329f |
| 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 |
|
| 75393 | 13 |
object XZ {
|
| 68018 | 14 |
/* options */ |
15 |
||
| 64002 | 16 |
type Options = LZMA2Options |
17 |
||
| 75393 | 18 |
def options(preset: Int = 3): Options = {
|
| 64000 | 19 |
val opts = new LZMA2Options |
20 |
opts.setPreset(preset) |
|
21 |
opts |
|
22 |
} |
|
| 68018 | 23 |
|
24 |
||
25 |
/* cache */ |
|
26 |
||
27 |
type Cache = ArrayCache |
|
28 |
||
| 75393 | 29 |
object Cache {
|
| 73024 | 30 |
def none: ArrayCache = ArrayCache.getDummyCache() |
31 |
def apply(): ArrayCache = ArrayCache.getDefaultCache() |
|
32 |
def make(): ArrayCache = new BasicArrayCache |
|
33 |
} |
|
| 75620 | 34 |
|
35 |
||
36 |
/* Scala functions in ML */ |
|
37 |
||
38 |
object Compress extends Scala.Fun_Bytes("XZ.compress") {
|
|
39 |
val here = Scala_Project.here |
|
40 |
def apply(arg: Bytes): Bytes = arg.compress() |
|
41 |
} |
|
42 |
||
43 |
object Uncompress extends Scala.Fun_Bytes("XZ.uncompress") {
|
|
44 |
val here = Scala_Project.here |
|
45 |
def apply(arg: Bytes): Bytes = arg.uncompress() |
|
46 |
} |
|
|
52671
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
47 |
} |