author | wenzelm |
Sun, 02 Oct 2016 22:05:40 +0200 | |
changeset 64000 | 445b3deced8f |
parent 52671 | src/Pure/General/xz_file.scala@9a360530eac8 |
child 64002 | 08f89f0e8a62 |
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 |
|
64000 | 4 |
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 |
|
64000 | 10 |
import java.io.{File => JFile, BufferedOutputStream, OutputStream, InputStream, BufferedInputStream} |
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 |
import org.tukaani.xz.{LZMA2Options, XZInputStream, XZOutputStream} |
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
13 |
|
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
14 |
|
64000 | 15 |
object XZ |
52671
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
16 |
{ |
64000 | 17 |
def options(preset: Int): LZMA2Options = |
18 |
{ |
|
19 |
val opts = new LZMA2Options |
|
20 |
opts.setPreset(preset) |
|
21 |
opts |
|
22 |
} |
|
52671
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
23 |
|
64000 | 24 |
def write_file(file: JFile, text: Iterable[CharSequence], preset: Int = 3) |
52671
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
25 |
{ |
64000 | 26 |
val opts = options(preset) |
27 |
File.write_file(file, text, |
|
28 |
(s: OutputStream) => new XZOutputStream(new BufferedOutputStream(s), opts)) |
|
52671
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
29 |
} |
64000 | 30 |
|
31 |
def uncompress(s: InputStream): XZInputStream = new XZInputStream(new BufferedInputStream(s)) |
|
52671
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
32 |
} |