6 */ |
6 */ |
7 |
7 |
8 package isabelle |
8 package isabelle |
9 |
9 |
10 import java.lang.System |
10 import java.lang.System |
11 import java.util.zip.{ZipEntry, ZipInputStream} |
|
12 import java.util.regex.Pattern |
11 import java.util.regex.Pattern |
13 import java.util.Locale |
12 import java.util.Locale |
14 import java.net.URL |
13 import java.net.URL |
15 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream, |
14 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream, |
16 BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader, |
15 BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader, |
178 (output, rc) |
177 (output, rc) |
179 } |
178 } |
180 |
179 |
181 def raw_exec(cwd: File, env: Map[String, String], redirect: Boolean, args: String*) |
180 def raw_exec(cwd: File, env: Map[String, String], redirect: Boolean, args: String*) |
182 : (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*)) |
181 : (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*)) |
183 |
|
184 |
|
185 /* unpack zip archive -- platform file-system */ |
|
186 |
|
187 def unzip(url: URL, root: File) |
|
188 { |
|
189 import scala.collection.JavaConversions._ |
|
190 |
|
191 val buffer = new Array[Byte](4096) |
|
192 |
|
193 val zip_stream = new ZipInputStream(new BufferedInputStream(url.openStream)) |
|
194 var entry: ZipEntry = null |
|
195 try { |
|
196 while ({ entry = zip_stream.getNextEntry; entry != null }) { |
|
197 val file = new File(root, entry.getName.replace('/', File.separatorChar)) |
|
198 val dir = file.getParentFile |
|
199 if (dir != null && !dir.isDirectory && !dir.mkdirs) |
|
200 error("Failed to create directory: " + dir) |
|
201 |
|
202 var len = 0 |
|
203 val out_stream = new BufferedOutputStream(new FileOutputStream(file)) |
|
204 try { |
|
205 while ({ len = zip_stream.read(buffer); len != -1 }) |
|
206 out_stream.write(buffer, 0, len) |
|
207 } |
|
208 finally { out_stream.close } |
|
209 } |
|
210 } |
|
211 finally { zip_stream.close } |
|
212 } |
|
213 |
|
214 |
|
215 /* unpack tar archive -- POSIX file-system */ |
|
216 |
|
217 def posix_untar(url: URL, root: File, gunzip: Boolean = false, |
|
218 tar: String = "tar", gzip: String = "", progress: Int => Unit = _ => ()): String = |
|
219 { |
|
220 if (!root.isDirectory && !root.mkdirs) |
|
221 error("Failed to create root directory: " + root) |
|
222 |
|
223 val connection = url.openConnection |
|
224 |
|
225 val length = connection.getContentLength.toLong |
|
226 require(length >= 0L) |
|
227 |
|
228 val stream = new BufferedInputStream(connection.getInputStream) |
|
229 val progress_stream = new InputStream { |
|
230 private val total = length max 1L |
|
231 private var index = 0L |
|
232 private var percentage = 0L |
|
233 override def read(): Int = |
|
234 { |
|
235 val c = stream.read |
|
236 if (c != -1) { |
|
237 index += 100 |
|
238 val p = index / total |
|
239 if (percentage != p) { percentage = p; progress(percentage.toInt) } |
|
240 } |
|
241 c |
|
242 } |
|
243 override def available(): Int = stream.available |
|
244 override def close() { stream.close } |
|
245 } |
|
246 |
|
247 val cmdline = |
|
248 List(tar, "-o", "-x", "-f-") ::: |
|
249 (if (!gunzip) Nil else if (gzip == "") List("-z") else List("-I", gzip)) |
|
250 |
|
251 val proc = raw_execute(root, null, false, cmdline:_*) |
|
252 val stdout = Simple_Thread.future("tar_stdout") { slurp(proc.getInputStream) } |
|
253 val stderr = Simple_Thread.future("tar_stderr") { slurp(proc.getErrorStream) } |
|
254 val stdin = new BufferedOutputStream(proc.getOutputStream) |
|
255 |
|
256 try { |
|
257 var c = -1 |
|
258 val io_err = |
|
259 try { while ({ c = progress_stream.read; c != -1 }) stdin.write(c); false } |
|
260 catch { case e: IOException => true } |
|
261 stdin.close |
|
262 |
|
263 val rc = try { proc.waitFor } finally { Thread.interrupted } |
|
264 if (io_err || rc != 0) error(stderr.join.trim) else stdout.join |
|
265 } |
|
266 finally { |
|
267 progress_stream.close |
|
268 stdin.close |
|
269 proc.destroy |
|
270 } |
|
271 } |
|
272 |
182 |
273 |
183 |
274 /* cygwin_root */ |
184 /* cygwin_root */ |
275 |
185 |
276 def cygwin_root(): String = |
186 def cygwin_root(): String = |