author | blanchet |
Thu, 11 Sep 2014 18:54:36 +0200 | |
changeset 58299 | 30ab8289f0e1 |
parent 52671 | 9a360530eac8 |
permissions | -rw-r--r-- |
52671
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/General/xz_file.scala |
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 |
|
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
4 |
XZ file system operations. |
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 |
|
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
10 |
import java.io.{BufferedOutputStream, OutputStream, FileInputStream, BufferedInputStream, |
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
11 |
File => JFile} |
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
12 |
|
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
13 |
import org.tukaani.xz.{LZMA2Options, XZInputStream, XZOutputStream} |
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
14 |
|
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
15 |
|
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
16 |
object XZ_File |
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
17 |
{ |
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
18 |
def read(file: JFile): String = |
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
19 |
File.read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file)))) |
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
20 |
|
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
21 |
def read(path: Path): String = read(path.file) |
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
22 |
|
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
23 |
def write(file: JFile, text: Iterable[CharSequence], preset: Int = 3) |
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
24 |
{ |
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
25 |
val options = new LZMA2Options |
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
26 |
options.setPreset(preset) |
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
27 |
File.write_file(file, text, (s: OutputStream) => |
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
28 |
new XZOutputStream(new BufferedOutputStream(s), options)) |
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
29 |
} |
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
30 |
} |
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff
changeset
|
31 |