| author | nipkow | 
| Mon, 16 Nov 2015 15:59:47 +0100 | |
| changeset 61688 | d04b1b4fb015 | 
| 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  |