35 def read(path: Path): String = read(path.file) |
35 def read(path: Path): String = read(path.file) |
36 |
36 |
37 |
37 |
38 /* write */ |
38 /* write */ |
39 |
39 |
40 private def write_file(file: JFile, text: CharSequence, zip: Boolean) |
40 private def write_file(file: JFile, text: CharSequence, gzip: Boolean) |
41 { |
41 { |
42 val stream1 = new FileOutputStream(file) |
42 val stream1 = new FileOutputStream(file) |
43 val stream2 = if (zip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1 |
43 val stream2 = if (gzip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1 |
44 val writer = new BufferedWriter(new OutputStreamWriter(stream2, Standard_System.charset)) |
44 val writer = new BufferedWriter(new OutputStreamWriter(stream2, Standard_System.charset)) |
45 try { writer.append(text) } |
45 try { writer.append(text) } |
46 finally { writer.close } |
46 finally { writer.close } |
47 } |
47 } |
48 |
48 |
49 def write(file: JFile, text: CharSequence): Unit = write_file(file, text, false) |
49 def write(file: JFile, text: CharSequence): Unit = write_file(file, text, false) |
50 def write(path: Path, text: CharSequence): Unit = write(path.file, text) |
50 def write(path: Path, text: CharSequence): Unit = write(path.file, text) |
51 |
51 |
52 def write_zip(file: JFile, text: CharSequence): Unit = write_file(file, text, true) |
52 def write_gzip(file: JFile, text: CharSequence): Unit = write_file(file, text, true) |
53 def write_zip(path: Path, text: CharSequence): Unit = write_zip(path.file, text) |
53 def write_gzip(path: Path, text: CharSequence): Unit = write_gzip(path.file, text) |
54 |
54 |
55 |
55 |
56 /* copy */ |
56 /* copy */ |
57 |
57 |
58 def eq(file1: JFile, file2: JFile): Boolean = |
58 def eq(file1: JFile, file2: JFile): Boolean = |