added Standard_System.raw_untar;
authorwenzelm
Sun Sep 26 22:54:37 2010 +0200 (2010-09-26)
changeset 3970541e9f69c553d
parent 39704 b4e0bddc9e4c
child 39706 6e74fb2d4374
added Standard_System.raw_untar;
src/Pure/System/standard_system.scala
     1.1 --- a/src/Pure/System/standard_system.scala	Sun Sep 26 19:46:02 2010 +0200
     1.2 +++ b/src/Pure/System/standard_system.scala	Sun Sep 26 22:54:37 2010 +0200
     1.3 @@ -8,7 +8,9 @@
     1.4  
     1.5  import java.util.regex.Pattern
     1.6  import java.util.Locale
     1.7 -import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream,
     1.8 +import java.util.zip.GZIPInputStream
     1.9 +import java.net.URL
    1.10 +import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
    1.11    BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader,
    1.12    File, FileFilter, IOException}
    1.13  
    1.14 @@ -154,6 +156,58 @@
    1.15  
    1.16    def raw_exec(cwd: File, env: Map[String, String], redirect: Boolean, args: String*)
    1.17      : (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*))
    1.18 +
    1.19 +
    1.20 +  /* unpack tar.gz */
    1.21 +
    1.22 +  def raw_untar(url: URL, root: File,
    1.23 +    tar: String = "tar", progress: Int => Unit = _ => ()): String =
    1.24 +  {
    1.25 +    if (!root.isDirectory && !root.mkdirs) error("Failed to create root directory: " + root)
    1.26 +
    1.27 +    val connection = url.openConnection
    1.28 +
    1.29 +    val length = connection.getContentLength.toLong
    1.30 +    require(length >= 0L)
    1.31 +
    1.32 +    val buffered_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 +        if (c != -1) {
    1.41 +          index += 100
    1.42 +          val p = index / total
    1.43 +          if (percentage != p) { percentage = p; progress(percentage.toInt) }
    1.44 +        }
    1.45 +        c
    1.46 +      }
    1.47 +      override def close() { buffered_stream.close }
    1.48 +    }
    1.49 +    val gzip_stream = new GZIPInputStream(progress_stream)
    1.50 +
    1.51 +    val proc = raw_execute(null, null, false, tar, "-C", root.getCanonicalPath, "-x", "-f", "-")
    1.52 +    val stdout = Simple_Thread.future("tar_stdout") { slurp(proc.getInputStream) }
    1.53 +    val stderr = Simple_Thread.future("tar_stderr") { slurp(proc.getErrorStream) }
    1.54 +    val stdin = new BufferedOutputStream(proc.getOutputStream)
    1.55 +
    1.56 +    try {
    1.57 +      var c = -1
    1.58 +      while ({ c = gzip_stream.read; c != -1 }) stdin.write(c)
    1.59 +      stdin.close
    1.60 +
    1.61 +      val rc = try { proc.waitFor } finally { Thread.interrupted }
    1.62 +      if (rc != 0) error(stderr.join.trim) else stdout.join
    1.63 +    }
    1.64 +    finally {
    1.65 +      gzip_stream.close
    1.66 +      stdin.close
    1.67 +      proc.destroy
    1.68 +    }
    1.69 +  }
    1.70  }
    1.71  
    1.72