6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
10 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream, |
10 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream, |
11 InputStream, FileInputStream, BufferedInputStream, BufferedReader, InputStreamReader, |
11 OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader, |
12 File => JFile, IOException} |
12 InputStreamReader, File => JFile, IOException} |
13 import java.util.zip.{GZIPInputStream, GZIPOutputStream} |
13 import java.util.zip.{GZIPInputStream, GZIPOutputStream} |
14 |
14 |
15 import scala.collection.mutable |
15 import scala.collection.mutable |
|
16 |
|
17 import org.tukaani.xz.{LZMA2Options, XZInputStream, XZOutputStream} |
16 |
18 |
17 |
19 |
18 object File |
20 object File |
19 { |
21 { |
20 /* directory content */ |
22 /* directory content */ |
70 def read_stream(stream: InputStream): String = |
72 def read_stream(stream: InputStream): String = |
71 read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset))) |
73 read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset))) |
72 |
74 |
73 def read_gzip(file: JFile): String = |
75 def read_gzip(file: JFile): String = |
74 read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file)))) |
76 read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file)))) |
|
77 |
75 def read_gzip(path: Path): String = read_gzip(path.file) |
78 def read_gzip(path: Path): String = read_gzip(path.file) |
|
79 |
|
80 def read_xz(file: JFile): String = |
|
81 read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file)))) |
|
82 |
|
83 def read_xz(path: Path): String = read_xz(path.file) |
76 |
84 |
77 |
85 |
78 /* read lines */ |
86 /* read lines */ |
79 |
87 |
80 def read_lines(reader: BufferedReader, progress: String => Unit): List[String] = |
88 def read_lines(reader: BufferedReader, progress: String => Unit): List[String] = |
103 } |
111 } |
104 |
112 |
105 |
113 |
106 /* write */ |
114 /* write */ |
107 |
115 |
108 private def write_file(file: JFile, text: CharSequence, gzip: Boolean) |
116 private def write_file(file: JFile, text: CharSequence, make_stream: OutputStream => OutputStream) |
109 { |
117 { |
110 val stream1 = new FileOutputStream(file) |
118 val stream = make_stream(new FileOutputStream(file)) |
111 val stream2 = if (gzip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1 |
119 val writer = new BufferedWriter(new OutputStreamWriter(stream, UTF8.charset)) |
112 val writer = new BufferedWriter(new OutputStreamWriter(stream2, UTF8.charset)) |
120 try { writer.append(text) } finally { writer.close } |
113 try { writer.append(text) } |
|
114 finally { writer.close } |
|
115 } |
121 } |
116 |
122 |
117 def write(file: JFile, text: CharSequence): Unit = write_file(file, text, false) |
123 def write(file: JFile, text: CharSequence): Unit = write_file(file, text, (s) => s) |
|
124 |
118 def write(path: Path, text: CharSequence): Unit = write(path.file, text) |
125 def write(path: Path, text: CharSequence): Unit = write(path.file, text) |
119 |
126 |
120 def write_gzip(file: JFile, text: CharSequence): Unit = write_file(file, text, true) |
127 def write_gzip(file: JFile, text: CharSequence): Unit = |
|
128 write_file(file, text, (s: OutputStream) => new GZIPOutputStream(new BufferedOutputStream(s))) |
|
129 |
121 def write_gzip(path: Path, text: CharSequence): Unit = write_gzip(path.file, text) |
130 def write_gzip(path: Path, text: CharSequence): Unit = write_gzip(path.file, text) |
|
131 |
|
132 def write_xz(file: JFile, text: CharSequence, preset: Int) |
|
133 { |
|
134 val options = new LZMA2Options |
|
135 options.setPreset(preset) |
|
136 write_file(file, text, (s: OutputStream) => |
|
137 new XZOutputStream(new BufferedOutputStream(s), options)) |
|
138 } |
|
139 |
|
140 def write_xz(file: JFile, text: CharSequence): Unit = |
|
141 write_xz(file, text, LZMA2Options.PRESET_DEFAULT) |
|
142 |
|
143 def write_xz(path: Path, text: CharSequence, preset: Int): Unit = |
|
144 write_xz(path.file, text, preset) |
|
145 |
|
146 def write_xz(path: Path, text: CharSequence): Unit = |
|
147 write_xz(path.file, text, LZMA2Options.PRESET_DEFAULT) |
122 |
148 |
123 |
149 |
124 /* copy */ |
150 /* copy */ |
125 |
151 |
126 def eq(file1: JFile, file2: JFile): Boolean = |
152 def eq(file1: JFile, file2: JFile): Boolean = |