equal
deleted
inserted
replaced
1 /* Title: Pure/General/xz.scala |
1 /* Title: Pure/General/xz.scala |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 XZ data compression. |
4 Support for XZ data compression. |
5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
10 import java.io.{File => JFile, BufferedOutputStream, OutputStream, InputStream, BufferedInputStream} |
10 import org.tukaani.xz.LZMA2Options |
11 |
|
12 import org.tukaani.xz.{LZMA2Options, XZInputStream, XZOutputStream} |
|
13 |
11 |
14 |
12 |
15 object XZ |
13 object XZ |
16 { |
14 { |
17 def options(preset: Int): LZMA2Options = |
15 type Options = LZMA2Options |
|
16 |
|
17 def options(): Options = options_preset(3) |
|
18 |
|
19 def options_preset(preset: Int): Options = |
18 { |
20 { |
19 val opts = new LZMA2Options |
21 val opts = new LZMA2Options |
20 opts.setPreset(preset) |
22 opts.setPreset(preset) |
21 opts |
23 opts |
22 } |
24 } |
23 |
|
24 def write_file(file: JFile, text: Iterable[CharSequence], preset: Int = 3) |
|
25 { |
|
26 val opts = options(preset) |
|
27 File.write_file(file, text, |
|
28 (s: OutputStream) => new XZOutputStream(new BufferedOutputStream(s), opts)) |
|
29 } |
|
30 |
|
31 def uncompress(s: InputStream): XZInputStream = new XZInputStream(new BufferedInputStream(s)) |
|
32 } |
25 } |