7 package isabelle |
7 package isabelle |
8 |
8 |
9 import java.util.regex.Pattern |
9 import java.util.regex.Pattern |
10 import java.util.Locale |
10 import java.util.Locale |
11 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, |
11 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, |
12 BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader, |
12 BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader, |
13 File, FileFilter, IOException} |
13 File, FileFilter, IOException} |
14 |
14 |
15 import scala.io.{Source, Codec} |
15 import scala.io.{Source, Codec} |
16 import scala.util.matching.Regex |
16 import scala.util.matching.Regex |
17 import scala.collection.mutable |
17 import scala.collection.mutable |
75 } |
75 } |
76 |
76 |
77 |
77 |
78 /* basic file operations */ |
78 /* basic file operations */ |
79 |
79 |
80 def with_tmp_file[A](prefix: String)(body: File => A): A = |
80 def slurp(reader: BufferedReader): String = |
81 { |
81 { |
82 val file = File.createTempFile(prefix, null) |
82 val output = new StringBuilder(100) |
83 try { body(file) } finally { file.delete } |
83 var c = -1 |
84 } |
84 while ({ c = reader.read; c != -1 }) output += c.toChar |
85 |
|
86 def read_file(file: File): String = |
|
87 { |
|
88 val buf = new StringBuilder(file.length.toInt) |
|
89 val reader = new BufferedReader(new InputStreamReader(new FileInputStream(file), charset)) |
|
90 var c = reader.read |
|
91 while (c != -1) { |
|
92 buf.append(c.toChar) |
|
93 c = reader.read |
|
94 } |
|
95 reader.close |
85 reader.close |
96 buf.toString |
86 output.toString |
97 } |
87 } |
|
88 |
|
89 def slurp(stream: InputStream): String = |
|
90 slurp(new BufferedReader(new InputStreamReader(stream, charset))) |
|
91 |
|
92 def read_file(file: File): String = slurp(new FileInputStream(file)) |
98 |
93 |
99 def write_file(file: File, text: CharSequence) |
94 def write_file(file: File, text: CharSequence) |
100 { |
95 { |
101 val writer = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), charset)) |
96 val writer = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), charset)) |
102 try { writer.append(text) } |
97 try { writer.append(text) } |
103 finally { writer.close } |
98 finally { writer.close } |
|
99 } |
|
100 |
|
101 def with_tmp_file[A](prefix: String)(body: File => A): A = |
|
102 { |
|
103 val file = File.createTempFile(prefix, null) |
|
104 try { body(file) } finally { file.delete } |
104 } |
105 } |
105 |
106 |
106 // FIXME handle (potentially cyclic) directory graph |
107 // FIXME handle (potentially cyclic) directory graph |
107 def find_files(start: File, ok: File => Boolean): List[File] = |
108 def find_files(start: File, ok: File => Boolean): List[File] = |
108 { |
109 { |
136 } |
137 } |
137 |
138 |
138 def process_output(proc: Process): (String, Int) = |
139 def process_output(proc: Process): (String, Int) = |
139 { |
140 { |
140 proc.getOutputStream.close |
141 proc.getOutputStream.close |
141 val output = Source.fromInputStream(proc.getInputStream)(codec()).mkString // FIXME |
142 val output = slurp(proc.getInputStream) |
142 val rc = |
143 val rc = |
143 try { proc.waitFor } |
144 try { proc.waitFor } |
144 finally { |
145 finally { |
145 proc.getInputStream.close |
146 proc.getInputStream.close |
146 proc.getErrorStream.close |
147 proc.getErrorStream.close |