# HG changeset patch
# User wenzelm
# Date 1338362737 -7200
# Node ID 69ba790960ba37734793704200cd5a777ebff703
# Parent  8559d681a617fa2562c1c2f19f7714ad78251fd7
discontinued unused unzip/untar;

diff -r 8559d681a617 -r 69ba790960ba src/Pure/System/standard_system.scala
--- a/src/Pure/System/standard_system.scala	Tue May 29 23:19:37 2012 +0200
+++ b/src/Pure/System/standard_system.scala	Wed May 30 09:25:37 2012 +0200
@@ -8,7 +8,6 @@
 package isabelle
 
 import java.lang.System
-import java.util.zip.{ZipEntry, ZipInputStream}
 import java.util.regex.Pattern
 import java.util.Locale
 import java.net.URL
@@ -182,95 +181,6 @@
     : (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*))
 
 
-  /* unpack zip archive -- platform file-system */
-
-  def unzip(url: URL, root: File)
-  {
-    import scala.collection.JavaConversions._
-
-    val buffer = new Array[Byte](4096)
-
-    val zip_stream = new ZipInputStream(new BufferedInputStream(url.openStream))
-    var entry: ZipEntry = null
-    try {
-      while ({ entry = zip_stream.getNextEntry; entry != null }) {
-        val file = new File(root, entry.getName.replace('/', File.separatorChar))
-        val dir = file.getParentFile
-        if (dir != null && !dir.isDirectory && !dir.mkdirs)
-          error("Failed to create directory: " + dir)
-
-        var len = 0
-        val out_stream = new BufferedOutputStream(new FileOutputStream(file))
-        try {
-          while ({ len = zip_stream.read(buffer); len != -1 })
-            out_stream.write(buffer, 0, len)
-        }
-        finally { out_stream.close }
-      }
-    }
-    finally { zip_stream.close }
-  }
-
-
-  /* unpack tar archive -- POSIX file-system */
-
-  def posix_untar(url: URL, root: File, gunzip: Boolean = false,
-    tar: String = "tar", gzip: String = "", progress: Int => Unit = _ => ()): String =
-  {
-    if (!root.isDirectory && !root.mkdirs)
-      error("Failed to create root directory: " + root)
-
-    val connection = url.openConnection
-
-    val length = connection.getContentLength.toLong
-    require(length >= 0L)
-
-    val stream = new BufferedInputStream(connection.getInputStream)
-    val progress_stream = new InputStream {
-      private val total = length max 1L
-      private var index = 0L
-      private var percentage = 0L
-      override def read(): Int =
-      {
-        val c = stream.read
-        if (c != -1) {
-          index += 100
-          val p = index / total
-          if (percentage != p) { percentage = p; progress(percentage.toInt) }
-        }
-        c
-      }
-      override def available(): Int = stream.available
-      override def close() { stream.close }
-    }
-
-    val cmdline =
-      List(tar, "-o", "-x", "-f-") :::
-        (if (!gunzip) Nil else if (gzip == "") List("-z") else List("-I", gzip))
-
-    val proc = raw_execute(root, null, false, cmdline:_*)
-    val stdout = Simple_Thread.future("tar_stdout") { slurp(proc.getInputStream) }
-    val stderr = Simple_Thread.future("tar_stderr") { slurp(proc.getErrorStream) }
-    val stdin = new BufferedOutputStream(proc.getOutputStream)
-
-    try {
-      var c = -1
-      val io_err =
-        try { while ({ c = progress_stream.read; c != -1 }) stdin.write(c); false }
-        catch { case e: IOException => true }
-      stdin.close
-
-      val rc = try { proc.waitFor } finally { Thread.interrupted }
-      if (io_err || rc != 0) error(stderr.join.trim) else stdout.join
-    }
-    finally {
-      progress_stream.close
-      stdin.close
-      proc.destroy
-    }
-  }
-
-
   /* cygwin_root */
 
   def cygwin_root(): String =