author | wenzelm |
Tue, 24 Jul 2012 23:01:55 +0200 | |
changeset 48494 | 00eb5be9e76b |
parent 48418 | 1a634f9614fb |
child 48550 | 97592027a2a8 |
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, |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
11 |
InputStream, FileInputStream, BufferedReader, InputStreamReader, File => JFile, FileFilter} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
12 |
import java.util.zip.GZIPOutputStream |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
13 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
14 |
import scala.collection.mutable |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
15 |
|
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 |
object File |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
18 |
{ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
19 |
/* read */ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
20 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
21 |
def read(reader: BufferedReader): String = |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
22 |
{ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
23 |
val output = new StringBuilder(100) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
24 |
var c = -1 |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
25 |
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
|
26 |
reader.close |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
27 |
output.toString |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
28 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
29 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
30 |
def read(stream: InputStream): String = |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
31 |
read(new BufferedReader(new InputStreamReader(stream, Standard_System.charset))) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
32 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
33 |
def read(file: JFile): String = read(new FileInputStream(file)) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
34 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
35 |
def read(path: Path): String = read(path.file) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
36 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
37 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
38 |
/* write */ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
39 |
|
48494 | 40 |
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
|
41 |
{ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
42 |
val stream1 = new FileOutputStream(file) |
48494 | 43 |
val stream2 = if (gzip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1 |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
44 |
val writer = new BufferedWriter(new OutputStreamWriter(stream2, Standard_System.charset)) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
45 |
try { writer.append(text) } |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
46 |
finally { writer.close } |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
47 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
48 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
49 |
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
|
50 |
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
|
51 |
|
48494 | 52 |
def write_gzip(file: JFile, text: CharSequence): Unit = write_file(file, text, true) |
53 |
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
|
54 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
55 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
56 |
/* copy */ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
57 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
58 |
def eq(file1: JFile, file2: JFile): Boolean = |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
59 |
file1.getCanonicalPath == file2.getCanonicalPath // FIXME prefer java.nio.file.Files.isSameFile of Java 1.7 |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
60 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
61 |
def copy(src: JFile, dst: JFile) |
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 |
if (!eq(src, dst)) { |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
64 |
val in = new FileInputStream(src) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
65 |
try { |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
66 |
val out = new FileOutputStream(dst) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
67 |
try { |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
68 |
val buf = new Array[Byte](65536) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
69 |
var m = 0 |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
70 |
do { |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
71 |
m = in.read(buf, 0, buf.length) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
72 |
if (m != -1) out.write(buf, 0, m) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
73 |
} while (m != -1) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
74 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
75 |
finally { out.close } |
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 |
finally { in.close } |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
78 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
79 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
80 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
81 |
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
|
82 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
83 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
84 |
/* misc */ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
85 |
|
48418 | 86 |
def tmp_file(prefix: String): JFile = |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
87 |
{ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
88 |
val file = JFile.createTempFile(prefix, null) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
89 |
file.deleteOnExit |
48418 | 90 |
file |
91 |
} |
|
92 |
||
93 |
def with_tmp_file[A](prefix: String)(body: JFile => A): A = |
|
94 |
{ |
|
95 |
val file = tmp_file(prefix) |
|
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
96 |
try { body(file) } finally { file.delete } |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
97 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
98 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
99 |
// FIXME handle (potentially cyclic) directory graph |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
100 |
def find_files(start: JFile, ok: JFile => Boolean): List[JFile] = |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
101 |
{ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
102 |
val files = new mutable.ListBuffer[JFile] |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
103 |
val filter = new FileFilter { def accept(entry: JFile) = entry.isDirectory || ok(entry) } |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
104 |
def find_entry(entry: JFile) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
105 |
{ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
106 |
if (ok(entry)) files += entry |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
107 |
if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
108 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
109 |
find_entry(start) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
110 |
files.toList |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
111 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
112 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
113 |