author | wenzelm |
Sat, 23 Feb 2013 12:28:18 +0100 | |
changeset 51251 | d55cce4d72dd |
parent 50845 | 477ca927676f |
child 51504 | 18095684c5a6 |
permissions | -rw-r--r-- |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/General/file.scala |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
3 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
4 |
File system operations. |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
6 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
8 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
9 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
10 |
import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream, |
50684
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
11 |
InputStream, FileInputStream, BufferedInputStream, BufferedReader, InputStreamReader, |
51251
d55cce4d72dd
more permissive File.read_lines, which is relevant for Managed_Process join/kill;
wenzelm
parents:
50845
diff
changeset
|
12 |
File => JFile, IOException} |
50684
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
13 |
import java.util.zip.{GZIPInputStream, GZIPOutputStream} |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
14 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
15 |
import scala.collection.mutable |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
16 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
17 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
18 |
object File |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
19 |
{ |
48613
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
20 |
/* directory content */ |
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
21 |
|
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
22 |
def read_dir(dir: Path): List[String] = |
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
23 |
{ |
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
24 |
if (!dir.is_dir) error("Bad directory: " + dir.toString) |
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
25 |
val files = dir.file.listFiles |
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
26 |
if (files == null) Nil |
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
27 |
else files.toList.map(_.getName) |
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
28 |
} |
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
29 |
|
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
30 |
def find_files(dir: Path): Stream[Path] = |
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
31 |
read_dir(dir).toStream.map(name => { |
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
32 |
val path = dir + Path.basic(name) |
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
33 |
path #:: (if (path.is_dir) find_files(path) else Stream.empty) |
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
34 |
}).flatten |
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
35 |
|
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
36 |
|
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
37 |
/* read */ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
38 |
|
48913
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
39 |
def read_bytes(file: JFile): Array[Byte] = |
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
40 |
{ |
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
41 |
var i = 0 |
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
42 |
var m = 0 |
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
43 |
val n = file.length.toInt |
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
44 |
val buf = new Array[Byte](n) |
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
45 |
|
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
46 |
val stream = new FileInputStream(file) |
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
47 |
try { |
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
48 |
do { |
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
49 |
m = stream.read(buf, i, n - i) |
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
50 |
if (m != -1) i += m |
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
51 |
} while (m != -1 && n > i) |
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
52 |
} |
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
53 |
finally { stream.close } |
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
54 |
buf |
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
55 |
} |
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
56 |
|
50203 | 57 |
def read(file: JFile): String = new String(read_bytes(file), UTF8.charset) |
48913
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
58 |
def read(path: Path): String = read(path.file) |
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
59 |
|
50684
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
60 |
|
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
61 |
def read_stream(reader: BufferedReader): String = |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
62 |
{ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
63 |
val output = new StringBuilder(100) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
64 |
var c = -1 |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
65 |
while ({ c = reader.read; c != -1 }) output += c.toChar |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
66 |
reader.close |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
67 |
output.toString |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
68 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
69 |
|
50684
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
70 |
def read_stream(stream: InputStream): String = |
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
71 |
read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset))) |
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
72 |
|
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
73 |
def read_gzip(file: JFile): String = |
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
74 |
read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file)))) |
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
75 |
def read_gzip(path: Path): String = read_gzip(path.file) |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
76 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
77 |
|
50845 | 78 |
/* read lines */ |
79 |
||
80 |
def read_lines(reader: BufferedReader, progress: String => Unit): List[String] = |
|
81 |
{ |
|
82 |
val result = new mutable.ListBuffer[String] |
|
83 |
var line: String = null |
|
51251
d55cce4d72dd
more permissive File.read_lines, which is relevant for Managed_Process join/kill;
wenzelm
parents:
50845
diff
changeset
|
84 |
while ({ line = try { reader.readLine} catch { case _: IOException => null }; line != null }) { |
50845 | 85 |
progress(line) |
86 |
result += line |
|
87 |
} |
|
88 |
reader.close |
|
89 |
result.toList |
|
90 |
} |
|
91 |
||
92 |
||
48550 | 93 |
/* try_read */ |
94 |
||
95 |
def try_read(paths: Seq[Path]): String = |
|
96 |
{ |
|
97 |
val buf = new StringBuilder |
|
98 |
for (path <- paths if path.is_file) { |
|
99 |
buf.append(read(path)) |
|
100 |
buf.append('\n') |
|
101 |
} |
|
102 |
buf.toString |
|
103 |
} |
|
104 |
||
105 |
||
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
106 |
/* write */ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
107 |
|
48494 | 108 |
private def write_file(file: JFile, text: CharSequence, gzip: Boolean) |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
109 |
{ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
110 |
val stream1 = new FileOutputStream(file) |
48494 | 111 |
val stream2 = if (gzip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1 |
50203 | 112 |
val writer = new BufferedWriter(new OutputStreamWriter(stream2, UTF8.charset)) |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
113 |
try { writer.append(text) } |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
114 |
finally { writer.close } |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
115 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
116 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
117 |
def write(file: JFile, text: CharSequence): Unit = write_file(file, text, false) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
118 |
def write(path: Path, text: CharSequence): Unit = write(path.file, text) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
119 |
|
48494 | 120 |
def write_gzip(file: JFile, text: CharSequence): Unit = write_file(file, text, true) |
121 |
def write_gzip(path: Path, text: CharSequence): Unit = write_gzip(path.file, text) |
|
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
122 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
123 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
124 |
/* copy */ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
125 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
126 |
def eq(file1: JFile, file2: JFile): Boolean = |
49673
2a088cff1e7b
more robust File.eq, and thus File.copy of "~~/lib/logo/isabelle.gif";
wenzelm
parents:
49610
diff
changeset
|
127 |
try { java.nio.file.Files.isSameFile(file1.toPath, file2.toPath) } |
2a088cff1e7b
more robust File.eq, and thus File.copy of "~~/lib/logo/isabelle.gif";
wenzelm
parents:
49610
diff
changeset
|
128 |
catch { case ERROR(_) => false } |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
129 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
130 |
def copy(src: JFile, dst: JFile) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
131 |
{ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
132 |
if (!eq(src, dst)) { |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
133 |
val in = new FileInputStream(src) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
134 |
try { |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
135 |
val out = new FileOutputStream(dst) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
136 |
try { |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
137 |
val buf = new Array[Byte](65536) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
138 |
var m = 0 |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
139 |
do { |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
140 |
m = in.read(buf, 0, buf.length) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
141 |
if (m != -1) out.write(buf, 0, m) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
142 |
} while (m != -1) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
143 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
144 |
finally { out.close } |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
145 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
146 |
finally { in.close } |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
147 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
148 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
149 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
150 |
def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
151 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
152 |
|
48613
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
153 |
/* tmp files */ |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
154 |
|
48418 | 155 |
def tmp_file(prefix: String): JFile = |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
156 |
{ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
157 |
val file = JFile.createTempFile(prefix, null) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
158 |
file.deleteOnExit |
48418 | 159 |
file |
160 |
} |
|
161 |
||
162 |
def with_tmp_file[A](prefix: String)(body: JFile => A): A = |
|
163 |
{ |
|
164 |
val file = tmp_file(prefix) |
|
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
165 |
try { body(file) } finally { file.delete } |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
166 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
167 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
168 |