src/Pure/System/standard_system.scala
author wenzelm
Tue Nov 29 21:29:53 2011 +0100 (2011-11-29)
changeset 45673 cd41e3903fbf
parent 45667 546d78f0d81f
child 47113 b5a5662528fb
permissions -rw-r--r--
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
     1 /*  Title:      Pure/System/standard_system.scala
     2     Module:     PIDE
     3     Author:     Makarius
     4 
     5 Standard system operations, with basic Cygwin/Posix compatibility.
     6 */
     7 
     8 package isabelle
     9 
    10 import java.lang.System
    11 import java.util.zip.{ZipEntry, ZipInputStream}
    12 import java.util.regex.Pattern
    13 import java.util.Locale
    14 import java.net.URL
    15 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
    16   BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader,
    17   File, FileFilter, IOException}
    18 import java.nio.charset.Charset
    19 
    20 import scala.io.{Source, Codec}
    21 import scala.util.matching.Regex
    22 import scala.collection.mutable
    23 
    24 
    25 object Standard_System
    26 {
    27   /* UTF-8 charset */
    28 
    29   val charset_name: String = "UTF-8"
    30   val charset: Charset = Charset.forName(charset_name)
    31   def codec(): Codec = Codec(charset)
    32 
    33   def string_bytes(s: String): Array[Byte] = s.getBytes(charset)
    34 
    35 
    36   /* permissive UTF-8 decoding */
    37 
    38   // see also http://en.wikipedia.org/wiki/UTF-8#Description
    39   // overlong encodings enable byte-stuffing
    40 
    41   def decode_permissive_utf8(text: CharSequence): String =
    42   {
    43     val buf = new java.lang.StringBuilder(text.length)
    44     var code = -1
    45     var rest = 0
    46     def flush()
    47     {
    48       if (code != -1) {
    49         if (rest == 0 && Character.isValidCodePoint(code))
    50           buf.appendCodePoint(code)
    51         else buf.append('\uFFFD')
    52         code = -1
    53         rest = 0
    54       }
    55     }
    56     def init(x: Int, n: Int)
    57     {
    58       flush()
    59       code = x
    60       rest = n
    61     }
    62     def push(x: Int)
    63     {
    64       if (rest <= 0) init(x, -1)
    65       else {
    66         code <<= 6
    67         code += x
    68         rest -= 1
    69       }
    70     }
    71     for (i <- 0 until text.length) {
    72       val c = text.charAt(i)
    73       if (c < 128) { flush(); buf.append(c) }
    74       else if ((c & 0xC0) == 0x80) push(c & 0x3F)
    75       else if ((c & 0xE0) == 0xC0) init(c & 0x1F, 1)
    76       else if ((c & 0xF0) == 0xE0) init(c & 0x0F, 2)
    77       else if ((c & 0xF8) == 0xF0) init(c & 0x07, 3)
    78     }
    79     flush()
    80     buf.toString
    81   }
    82 
    83   private class Decode_Chars(decode: String => String,
    84     buffer: Array[Byte], start: Int, end: Int) extends CharSequence
    85   {
    86     def length: Int = end - start
    87     def charAt(i: Int): Char = (buffer(start + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
    88     def subSequence(i: Int, j: Int): CharSequence =
    89       new Decode_Chars(decode, buffer, start + i, start + j)
    90 
    91     // toString with adhoc decoding: abuse of CharSequence interface
    92     override def toString: String = decode(decode_permissive_utf8(this))
    93   }
    94 
    95   def decode_chars(decode: String => String,
    96     buffer: Array[Byte], start: Int, end: Int): CharSequence =
    97   {
    98     require(0 <= start && start <= end && end <= buffer.length)
    99     new Decode_Chars(decode, buffer, start, end)
   100   }
   101 
   102 
   103   /* basic file operations */
   104 
   105   def slurp(reader: BufferedReader): String =
   106   {
   107     val output = new StringBuilder(100)
   108     var c = -1
   109     while ({ c = reader.read; c != -1 }) output += c.toChar
   110     reader.close
   111     output.toString
   112   }
   113 
   114   def slurp(stream: InputStream): String =
   115     slurp(new BufferedReader(new InputStreamReader(stream, charset)))
   116 
   117   def read_file(file: File): String = slurp(new FileInputStream(file))
   118 
   119   def write_file(file: File, text: CharSequence)
   120   {
   121     val writer =
   122       new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), charset))
   123     try { writer.append(text) }
   124     finally { writer.close }
   125   }
   126 
   127   def with_tmp_file[A](prefix: String)(body: File => A): A =
   128   {
   129     val file = File.createTempFile(prefix, null)
   130     file.deleteOnExit
   131     try { body(file) } finally { file.delete }
   132   }
   133 
   134   // FIXME handle (potentially cyclic) directory graph
   135   def find_files(start: File, ok: File => Boolean): List[File] =
   136   {
   137     val files = new mutable.ListBuffer[File]
   138     val filter = new FileFilter { def accept(entry: File) = entry.isDirectory || ok(entry) }
   139     def find_entry(entry: File)
   140     {
   141       if (ok(entry)) files += entry
   142       if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry)
   143     }
   144     find_entry(start)
   145     files.toList
   146   }
   147 
   148 
   149   /* shell processes */
   150 
   151   def raw_execute(cwd: File, env: Map[String, String], redirect: Boolean, args: String*): Process =
   152   {
   153     val cmdline = new java.util.LinkedList[String]
   154     for (s <- args) cmdline.add(s)
   155 
   156     val proc = new ProcessBuilder(cmdline)
   157     if (cwd != null) proc.directory(cwd)
   158     if (env != null) {
   159       proc.environment.clear
   160       for ((x, y) <- env) proc.environment.put(x, y)
   161     }
   162     proc.redirectErrorStream(redirect)
   163     proc.start
   164   }
   165 
   166   def process_output(proc: Process): (String, Int) =
   167   {
   168     proc.getOutputStream.close
   169     val output = slurp(proc.getInputStream)
   170     val rc =
   171       try { proc.waitFor }
   172       finally {
   173         proc.getInputStream.close
   174         proc.getErrorStream.close
   175         proc.destroy
   176         Thread.interrupted
   177       }
   178     (output, rc)
   179   }
   180 
   181   def raw_exec(cwd: File, env: Map[String, String], redirect: Boolean, args: String*)
   182     : (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 }
   273 
   274 
   275 class Standard_System
   276 {
   277   /* platform_root */
   278 
   279   val platform_root = if (Platform.is_windows) Cygwin.check_root() else "/"
   280 
   281 
   282   /* jvm_path */
   283 
   284   private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
   285   private val Named_Root = new Regex("//+([^/]*)(.*)")
   286 
   287   def jvm_path(posix_path: String): String =
   288     if (Platform.is_windows) {
   289       val result_path = new StringBuilder
   290       val rest =
   291         posix_path match {
   292           case Cygdrive(drive, rest) =>
   293             result_path ++= (drive.toUpperCase(Locale.ENGLISH) + ":" + File.separator)
   294             rest
   295           case Named_Root(root, rest) =>
   296             result_path ++= File.separator
   297             result_path ++= File.separator
   298             result_path ++= root
   299             rest
   300           case path if path.startsWith("/") =>
   301             result_path ++= platform_root
   302             path
   303           case path => path
   304         }
   305       for (p <- space_explode('/', rest) if p != "") {
   306         val len = result_path.length
   307         if (len > 0 && result_path(len - 1) != File.separatorChar)
   308           result_path += File.separatorChar
   309         result_path ++= p
   310       }
   311       result_path.toString
   312     }
   313     else posix_path
   314 
   315 
   316   /* posix_path */
   317 
   318   private val Platform_Root = new Regex("(?i)" +
   319     Pattern.quote(platform_root) + """(?:\\+|\z)(.*)""")
   320 
   321   private val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
   322 
   323   def posix_path(jvm_path: String): String =
   324     if (Platform.is_windows) {
   325       jvm_path.replace('/', '\\') match {
   326         case Platform_Root(rest) => "/" + rest.replace('\\', '/')
   327         case Drive(letter, rest) =>
   328           "/cygdrive/" + letter.toLowerCase(Locale.ENGLISH) +
   329             (if (rest == "") "" else "/" + rest.replace('\\', '/'))
   330         case path => path.replace('\\', '/')
   331       }
   332     }
   333     else jvm_path
   334 
   335 
   336   /* this_java executable */
   337 
   338   def this_java(): String =
   339   {
   340     val java_home = System.getProperty("java.home")
   341     val java_exe =
   342       if (Platform.is_windows) new File(java_home + "\\bin\\java.exe")
   343       else new File(java_home + "/bin/java")
   344     if (!java_exe.isFile) error("Expected this Java executable: " + java_exe.toString)
   345     posix_path(java_exe.getAbsolutePath)
   346   }
   347 }