more efficient posix_untar -- avoid really slow java.util.zip.GZIPInputStream;
authorwenzelm
Mon Sep 27 13:38:35 2010 +0200 (2010-09-27)
changeset 39708c3239be617f4
parent 39707 4977324373f2
child 39709 1fa4c5c7d534
more efficient posix_untar -- avoid really slow java.util.zip.GZIPInputStream;
misc tuning;
src/Pure/System/standard_system.scala
     1.1 --- a/src/Pure/System/standard_system.scala	Mon Sep 27 11:31:39 2010 +0200
     1.2 +++ b/src/Pure/System/standard_system.scala	Mon Sep 27 13:38:35 2010 +0200
     1.3 @@ -8,7 +8,6 @@
     1.4  
     1.5  import java.util.regex.Pattern
     1.6  import java.util.Locale
     1.7 -import java.util.zip.GZIPInputStream
     1.8  import java.net.URL
     1.9  import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
    1.10    BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader,
    1.11 @@ -158,26 +157,27 @@
    1.12      : (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*))
    1.13  
    1.14  
    1.15 -  /* unpack tar.gz */
    1.16 +  /* unpack tar archive */
    1.17  
    1.18 -  def raw_untar(url: URL, root: File,
    1.19 +  def posix_untar(url: URL, root: File, gunzip: Boolean = false,
    1.20      tar: String = "tar", progress: Int => Unit = _ => ()): String =
    1.21    {
    1.22 -    if (!root.isDirectory && !root.mkdirs) error("Failed to create root directory: " + root)
    1.23 +    if (!root.isDirectory && !root.mkdirs)
    1.24 +      error("Failed to create root directory: " + root)
    1.25  
    1.26      val connection = url.openConnection
    1.27  
    1.28      val length = connection.getContentLength.toLong
    1.29      require(length >= 0L)
    1.30  
    1.31 -    val buffered_stream = new BufferedInputStream(connection.getInputStream)
    1.32 +    val stream = new BufferedInputStream(connection.getInputStream)
    1.33      val progress_stream = new InputStream {
    1.34        private val total = length max 1L
    1.35        private var index = 0L
    1.36        private var percentage = 0L
    1.37        override def read(): Int =
    1.38        {
    1.39 -        val c = buffered_stream.read
    1.40 +        val c = stream.read
    1.41          if (c != -1) {
    1.42            index += 100
    1.43            val p = index / total
    1.44 @@ -185,11 +185,11 @@
    1.45          }
    1.46          c
    1.47        }
    1.48 -      override def close() { buffered_stream.close }
    1.49 +      override def available(): Int = stream.available
    1.50 +      override def close() { stream.close }
    1.51      }
    1.52 -    val gzip_stream = new GZIPInputStream(progress_stream)
    1.53  
    1.54 -    val proc = raw_execute(root, null, false, tar, "-x", "-f", "-")
    1.55 +    val proc = raw_execute(root, null, false, tar, if (gunzip) "-xz" else "-x", "-f-")
    1.56      val stdout = Simple_Thread.future("tar_stdout") { slurp(proc.getInputStream) }
    1.57      val stderr = Simple_Thread.future("tar_stderr") { slurp(proc.getErrorStream) }
    1.58      val stdin = new BufferedOutputStream(proc.getOutputStream)
    1.59 @@ -197,7 +197,7 @@
    1.60      try {
    1.61        var c = -1
    1.62        val io_err =
    1.63 -        try { while ({ c = gzip_stream.read; c != -1 }) stdin.write(c); false }
    1.64 +        try { while ({ c = progress_stream.read; c != -1 }) stdin.write(c); false }
    1.65          catch { case e: IOException => true }
    1.66        stdin.close
    1.67  
    1.68 @@ -205,7 +205,7 @@
    1.69        if (io_err || rc != 0) error(stderr.join.trim) else stdout.join
    1.70      }
    1.71      finally {
    1.72 -      gzip_stream.close
    1.73 +      progress_stream.close
    1.74        stdin.close
    1.75        proc.destroy
    1.76      }