# HG changeset patch
# User wenzelm
# Date 1285604196 -7200
# Node ID 4dbc72759706b692424714f34d5d16d3e072a6db
# Parent  5cb0d7b0d601c4ce0e8530da9c076c255e6471e7
added Standard_System.unzip (for platform file-system);
tuned comments;

diff -r 5cb0d7b0d601 -r 4dbc72759706 src/Pure/System/standard_system.scala
--- a/src/Pure/System/standard_system.scala	Mon Sep 27 18:11:33 2010 +0200
+++ b/src/Pure/System/standard_system.scala	Mon Sep 27 18:16:36 2010 +0200
@@ -6,6 +6,7 @@
 
 package isabelle
 
+import java.util.zip.{ZipEntry, ZipInputStream}
 import java.util.regex.Pattern
 import java.util.Locale
 import java.net.URL
@@ -157,7 +158,37 @@
     : (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*))
 
 
-  /* unpack tar archive */
+  /* 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 =