9 |
9 |
10 import java.lang.System |
10 import java.lang.System |
11 import java.util.regex.Pattern |
11 import java.util.regex.Pattern |
12 import java.util.Locale |
12 import java.util.Locale |
13 import java.net.URL |
13 import java.net.URL |
14 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream, |
14 import java.io.{File => JFile} |
15 BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader, |
|
16 File => JFile, FileFilter, IOException} |
|
17 import java.nio.charset.Charset |
15 import java.nio.charset.Charset |
18 import java.util.zip.GZIPOutputStream |
|
19 |
16 |
20 import scala.io.Codec |
17 import scala.io.Codec |
21 import scala.util.matching.Regex |
18 import scala.util.matching.Regex |
22 import scala.collection.mutable |
|
23 |
19 |
24 |
20 |
25 object Standard_System |
21 object Standard_System |
26 { |
22 { |
27 /* UTF-8 charset */ |
23 /* UTF-8 charset */ |
98 require(0 <= start && start <= end && end <= buffer.length) |
94 require(0 <= start && start <= end && end <= buffer.length) |
99 new Decode_Chars(decode, buffer, start, end) |
95 new Decode_Chars(decode, buffer, start, end) |
100 } |
96 } |
101 |
97 |
102 |
98 |
103 /* basic file operations */ |
|
104 |
|
105 def slurp(reader: BufferedReader): String = |
|
106 { |
|
107 val output = new StringBuilder(100) |
|
108 var c = -1 |
|
109 while ({ c = reader.read; c != -1 }) output += c.toChar |
|
110 reader.close |
|
111 output.toString |
|
112 } |
|
113 |
|
114 def slurp(stream: InputStream): String = |
|
115 slurp(new BufferedReader(new InputStreamReader(stream, charset))) |
|
116 |
|
117 def read_file(file: JFile): String = slurp(new FileInputStream(file)) |
|
118 |
|
119 def write_file(file: JFile, text: CharSequence, zip: Boolean = false) |
|
120 { |
|
121 val stream1 = new FileOutputStream(file) |
|
122 val stream2 = if (zip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1 |
|
123 val writer = new BufferedWriter(new OutputStreamWriter(stream2, charset)) |
|
124 try { writer.append(text) } |
|
125 finally { writer.close } |
|
126 } |
|
127 |
|
128 def eq_file(file1: JFile, file2: JFile): Boolean = |
|
129 file1.getCanonicalPath == file2.getCanonicalPath // FIXME prefer java.nio.file.Files.isSameFile of Java 1.7 |
|
130 |
|
131 def copy_file(src: JFile, dst: JFile) = |
|
132 if (!eq_file(src, dst)) { |
|
133 val in = new FileInputStream(src) |
|
134 try { |
|
135 val out = new FileOutputStream(dst) |
|
136 try { |
|
137 val buf = new Array[Byte](65536) |
|
138 var m = 0 |
|
139 do { |
|
140 m = in.read(buf, 0, buf.length) |
|
141 if (m != -1) out.write(buf, 0, m) |
|
142 } while (m != -1) |
|
143 } |
|
144 finally { out.close } |
|
145 } |
|
146 finally { in.close } |
|
147 } |
|
148 |
|
149 def with_tmp_file[A](prefix: String)(body: JFile => A): A = |
|
150 { |
|
151 val file = JFile.createTempFile(prefix, null) |
|
152 file.deleteOnExit |
|
153 try { body(file) } finally { file.delete } |
|
154 } |
|
155 |
|
156 // FIXME handle (potentially cyclic) directory graph |
|
157 def find_files(start: JFile, ok: JFile => Boolean): List[JFile] = |
|
158 { |
|
159 val files = new mutable.ListBuffer[JFile] |
|
160 val filter = new FileFilter { def accept(entry: JFile) = entry.isDirectory || ok(entry) } |
|
161 def find_entry(entry: JFile) |
|
162 { |
|
163 if (ok(entry)) files += entry |
|
164 if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry) |
|
165 } |
|
166 find_entry(start) |
|
167 files.toList |
|
168 } |
|
169 |
|
170 |
|
171 /* shell processes */ |
99 /* shell processes */ |
172 |
100 |
173 def raw_execute(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process = |
101 def raw_execute(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process = |
174 { |
102 { |
175 val cmdline = new java.util.LinkedList[String] |
103 val cmdline = new java.util.LinkedList[String] |