src/Pure/System/standard_system.scala
author wenzelm
Sat Jan 02 01:14:49 2010 +0100 (2010-01-02 ago)
changeset 34219 d37cfca69887
parent 34202 99241daf807d
child 34258 e936d3c35ce0
permissions -rw-r--r--
Standard_System.raw_execute: optional cwd;
basic Cygwin.setup with download and unattended installation;
     1 /*  Title:      Pure/System/standard_system.scala
     2     Author:     Makarius
     3 
     4 Standard system operations, with basic Cygwin/Posix compatibility.
     5 */
     6 
     7 package isabelle
     8 
     9 import java.util.regex.Pattern
    10 import java.util.Locale
    11 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream,
    12   BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader,
    13   File, IOException}
    14 
    15 import scala.io.Source
    16 import scala.util.matching.Regex
    17 import scala.collection.mutable
    18 
    19 
    20 object Standard_System
    21 {
    22   val charset = "UTF-8"
    23 
    24 
    25   /* permissive UTF-8 decoding */
    26 
    27   // see also http://en.wikipedia.org/wiki/UTF-8#Description
    28   // overlong encodings enable byte-stuffing
    29 
    30   def decode_permissive_utf8(text: CharSequence): String =
    31   {
    32     val buf = new java.lang.StringBuilder(text.length)
    33     var code = -1
    34     var rest = 0
    35     def flush()
    36     {
    37       if (code != -1) {
    38         if (rest == 0 && Character.isValidCodePoint(code))
    39           buf.appendCodePoint(code)
    40         else buf.append('\uFFFD')
    41         code = -1
    42         rest = 0
    43       }
    44     }
    45     def init(x: Int, n: Int)
    46     {
    47       flush()
    48       code = x
    49       rest = n
    50     }
    51     def push(x: Int)
    52     {
    53       if (rest <= 0) init(x, -1)
    54       else {
    55         code <<= 6
    56         code += x
    57         rest -= 1
    58       }
    59     }
    60     for (i <- 0 until text.length) {
    61       val c = text.charAt(i)
    62       if (c < 128) { flush(); buf.append(c) }
    63       else if ((c & 0xC0) == 0x80) push(c & 0x3F)
    64       else if ((c & 0xE0) == 0xC0) init(c & 0x1F, 1)
    65       else if ((c & 0xF0) == 0xE0) init(c & 0x0F, 2)
    66       else if ((c & 0xF8) == 0xF0) init(c & 0x07, 3)
    67     }
    68     flush()
    69     buf.toString
    70   }
    71 
    72 
    73   /* basic file operations */
    74 
    75   def with_tmp_file[A](prefix: String)(body: File => A): A =
    76   {
    77     val file = File.createTempFile(prefix, null)
    78     try { body(file) } finally { file.delete }
    79   }
    80 
    81   def read_file(file: File): String =
    82   {
    83     val buf = new StringBuilder(file.length.toInt)
    84     val reader = new BufferedReader(new InputStreamReader(new FileInputStream(file), charset))
    85     var c = reader.read
    86     while (c != -1) {
    87       buf.append(c.toChar)
    88       c = reader.read
    89     }
    90     reader.close
    91     buf.toString
    92   }
    93 
    94   def write_file(file: File, text: CharSequence)
    95   {
    96     val writer = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), charset))
    97     try { writer.append(text) }
    98     finally { writer.close }
    99   }
   100 
   101 
   102   /* shell processes */
   103 
   104   def raw_execute(cwd: File, env: Map[String, String], redirect: Boolean, args: String*): Process =
   105   {
   106     val cmdline = new java.util.LinkedList[String]
   107     for (s <- args) cmdline.add(s)
   108 
   109     val proc = new ProcessBuilder(cmdline)
   110     if (cwd != null) proc.directory(cwd)
   111     if (env != null) {
   112       proc.environment.clear
   113       for ((x, y) <- env) proc.environment.put(x, y)
   114     }
   115     proc.redirectErrorStream(redirect)
   116 
   117     try { proc.start }
   118     catch { case e: IOException => error(e.getMessage) }
   119   }
   120 
   121   def process_output(proc: Process): (String, Int) =
   122   {
   123     proc.getOutputStream.close
   124     val output = Source.fromInputStream(proc.getInputStream, charset).mkString  // FIXME
   125     val rc =
   126       try { proc.waitFor }
   127       finally {
   128         proc.getInputStream.close
   129         proc.getErrorStream.close
   130         proc.destroy
   131         Thread.interrupted
   132       }
   133     (output, rc)
   134   }
   135 }
   136 
   137 
   138 class Standard_System
   139 {
   140   val platform_root = if (Platform.is_windows) Cygwin.check_root() else "/"
   141   override def toString = platform_root
   142 
   143 
   144   /* jvm_path */
   145 
   146   private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
   147 
   148   def jvm_path(posix_path: String): String =
   149     if (Platform.is_windows) {
   150       val result_path = new StringBuilder
   151       val rest =
   152         posix_path match {
   153           case Cygdrive(drive, rest) =>
   154             result_path ++= (drive + ":" + File.separator)
   155             rest
   156           case path if path.startsWith("/") =>
   157             result_path ++= platform_root
   158             path
   159           case path => path
   160         }
   161       for (p <- rest.split("/") if p != "") {
   162         val len = result_path.length
   163         if (len > 0 && result_path(len - 1) != File.separatorChar)
   164           result_path += File.separatorChar
   165         result_path ++= p
   166       }
   167       result_path.toString
   168     }
   169     else posix_path
   170 
   171 
   172   /* posix_path */
   173 
   174   private val Platform_Root = new Regex("(?i)" +
   175     Pattern.quote(platform_root) + """(?:\\+|\z)(.*)""")
   176 
   177   private val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
   178 
   179   def posix_path(jvm_path: String): String =
   180     if (Platform.is_windows) {
   181       jvm_path.replace('/', '\\') match {
   182         case Platform_Root(rest) => "/" + rest.replace('\\', '/')
   183         case Drive(letter, rest) =>
   184           "/cygdrive/" + letter.toLowerCase(Locale.ENGLISH) +
   185             (if (rest == "") "" else "/" + rest.replace('\\', '/'))
   186         case path => path.replace('\\', '/')
   187       }
   188     }
   189     else jvm_path
   190 }