|
1 /* Title: Pure/General/file.scala |
|
2 Author: Makarius |
|
3 |
|
4 File system operations. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream, |
|
11 InputStream, FileInputStream, BufferedReader, InputStreamReader, File => JFile, FileFilter} |
|
12 import java.util.zip.GZIPOutputStream |
|
13 |
|
14 import scala.collection.mutable |
|
15 |
|
16 |
|
17 object File |
|
18 { |
|
19 /* read */ |
|
20 |
|
21 def read(reader: BufferedReader): String = |
|
22 { |
|
23 val output = new StringBuilder(100) |
|
24 var c = -1 |
|
25 while ({ c = reader.read; c != -1 }) output += c.toChar |
|
26 reader.close |
|
27 output.toString |
|
28 } |
|
29 |
|
30 def read(stream: InputStream): String = |
|
31 read(new BufferedReader(new InputStreamReader(stream, Standard_System.charset))) |
|
32 |
|
33 def read(file: JFile): String = read(new FileInputStream(file)) |
|
34 |
|
35 def read(path: Path): String = read(path.file) |
|
36 |
|
37 |
|
38 /* write */ |
|
39 |
|
40 private def write_file(file: JFile, text: CharSequence, zip: Boolean) |
|
41 { |
|
42 val stream1 = new FileOutputStream(file) |
|
43 val stream2 = if (zip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1 |
|
44 val writer = new BufferedWriter(new OutputStreamWriter(stream2, Standard_System.charset)) |
|
45 try { writer.append(text) } |
|
46 finally { writer.close } |
|
47 } |
|
48 |
|
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) |
|
51 |
|
52 def write_zip(file: JFile, text: CharSequence): Unit = write_file(file, text, true) |
|
53 def write_zip(path: Path, text: CharSequence): Unit = write_zip(path.file, text) |
|
54 |
|
55 |
|
56 /* copy */ |
|
57 |
|
58 def eq(file1: JFile, file2: JFile): Boolean = |
|
59 file1.getCanonicalPath == file2.getCanonicalPath // FIXME prefer java.nio.file.Files.isSameFile of Java 1.7 |
|
60 |
|
61 def copy(src: JFile, dst: JFile) |
|
62 { |
|
63 if (!eq(src, dst)) { |
|
64 val in = new FileInputStream(src) |
|
65 try { |
|
66 val out = new FileOutputStream(dst) |
|
67 try { |
|
68 val buf = new Array[Byte](65536) |
|
69 var m = 0 |
|
70 do { |
|
71 m = in.read(buf, 0, buf.length) |
|
72 if (m != -1) out.write(buf, 0, m) |
|
73 } while (m != -1) |
|
74 } |
|
75 finally { out.close } |
|
76 } |
|
77 finally { in.close } |
|
78 } |
|
79 } |
|
80 |
|
81 def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file) |
|
82 |
|
83 |
|
84 /* misc */ |
|
85 |
|
86 def with_tmp_file[A](prefix: String)(body: JFile => A): A = |
|
87 { |
|
88 val file = JFile.createTempFile(prefix, null) |
|
89 file.deleteOnExit |
|
90 try { body(file) } finally { file.delete } |
|
91 } |
|
92 |
|
93 // FIXME handle (potentially cyclic) directory graph |
|
94 def find_files(start: JFile, ok: JFile => Boolean): List[JFile] = |
|
95 { |
|
96 val files = new mutable.ListBuffer[JFile] |
|
97 val filter = new FileFilter { def accept(entry: JFile) = entry.isDirectory || ok(entry) } |
|
98 def find_entry(entry: JFile) |
|
99 { |
|
100 if (ok(entry)) files += entry |
|
101 if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry) |
|
102 } |
|
103 find_entry(start) |
|
104 files.toList |
|
105 } |
|
106 } |
|
107 |