author | wenzelm |
Mon, 03 Oct 2016 10:51:51 +0200 | |
changeset 64002 | 08f89f0e8a62 |
parent 64000 | 445b3deced8f |
child 64004 | b4ece7a3f2ca |
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 |
|
64002 | 10 |
import org.tukaani.xz.LZMA2Options |
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 |
{ |
64002 | 15 |
type Options = LZMA2Options |
16 |
||
17 |
def options(): Options = options_preset(3) |
|
18 |
||
19 |
def options_preset(preset: Int): Options = |
|
64000 | 20 |
{ |
21 |
val opts = new LZMA2Options |
|
22 |
opts.setPreset(preset) |
|
23 |
opts |
|
24 |
} |
|
52671
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
25 |
} |