src/Pure/System/standard_system.scala
changeset 48027 69ba790960ba
parent 47998 969457d93f75
child 48277 f14e564fca1a
equal deleted inserted replaced
48026:8559d681a617 48027:69ba790960ba
     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 =