src/Pure/System/standard_system.scala
author wenzelm
Sat Sep 18 20:07:48 2010 +0200 (2010-09-18)
changeset 39522 01aade784da9
parent 38264 205b74a1bb18
child 39578 b75164153c37
permissions -rw-r--r--
raw_execute: let IOException pass-through unhindered (again);
     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, FileFilter, IOException}
    14 
    15 import scala.io.{Source, Codec}
    16 import scala.util.matching.Regex
    17 import scala.collection.mutable
    18 
    19 
    20 object Standard_System
    21 {
    22   /* UTF-8 charset */
    23 
    24   val charset = "UTF-8"
    25   def codec(): Codec = Codec(charset)
    26 
    27   def string_bytes(s: String): Array[Byte] = s.getBytes(charset)
    28 
    29 
    30   /* permissive UTF-8 decoding */
    31 
    32   // see also http://en.wikipedia.org/wiki/UTF-8#Description
    33   // overlong encodings enable byte-stuffing
    34 
    35   def decode_permissive_utf8(text: CharSequence): String =
    36   {
    37     val buf = new java.lang.StringBuilder(text.length)
    38     var code = -1
    39     var rest = 0
    40     def flush()
    41     {
    42       if (code != -1) {
    43         if (rest == 0 && Character.isValidCodePoint(code))
    44           buf.appendCodePoint(code)
    45         else buf.append('\uFFFD')
    46         code = -1
    47         rest = 0
    48       }
    49     }
    50     def init(x: Int, n: Int)
    51     {
    52       flush()
    53       code = x
    54       rest = n
    55     }
    56     def push(x: Int)
    57     {
    58       if (rest <= 0) init(x, -1)
    59       else {
    60         code <<= 6
    61         code += x
    62         rest -= 1
    63       }
    64     }
    65     for (i <- 0 until text.length) {
    66       val c = text.charAt(i)
    67       if (c < 128) { flush(); buf.append(c) }
    68       else if ((c & 0xC0) == 0x80) push(c & 0x3F)
    69       else if ((c & 0xE0) == 0xC0) init(c & 0x1F, 1)
    70       else if ((c & 0xF0) == 0xE0) init(c & 0x0F, 2)
    71       else if ((c & 0xF8) == 0xF0) init(c & 0x07, 3)
    72     }
    73     flush()
    74     buf.toString
    75   }
    76 
    77 
    78   /* basic file operations */
    79 
    80   def with_tmp_file[A](prefix: String)(body: File => A): A =
    81   {
    82     val file = File.createTempFile(prefix, null)
    83     try { body(file) } finally { file.delete }
    84   }
    85 
    86   def read_file(file: File): String =
    87   {
    88     val buf = new StringBuilder(file.length.toInt)
    89     val reader = new BufferedReader(new InputStreamReader(new FileInputStream(file), charset))
    90     var c = reader.read
    91     while (c != -1) {
    92       buf.append(c.toChar)
    93       c = reader.read
    94     }
    95     reader.close
    96     buf.toString
    97   }
    98 
    99   def write_file(file: File, text: CharSequence)
   100   {
   101     val writer = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), charset))
   102     try { writer.append(text) }
   103     finally { writer.close }
   104   }
   105 
   106   // FIXME handle (potentially cyclic) directory graph
   107   def find_files(start: File, ok: File => Boolean): List[File] =
   108   {
   109     val files = new mutable.ListBuffer[File]
   110     val filter = new FileFilter { def accept(entry: File) = entry.isDirectory || ok(entry) }
   111     def find_entry(entry: File)
   112     {
   113       if (ok(entry)) files += entry
   114       if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry)
   115     }
   116     find_entry(start)
   117     files.toList
   118   }
   119 
   120 
   121   /* shell processes */
   122 
   123   def raw_execute(cwd: File, env: Map[String, String], redirect: Boolean, args: String*): Process =
   124   {
   125     val cmdline = new java.util.LinkedList[String]
   126     for (s <- args) cmdline.add(s)
   127 
   128     val proc = new ProcessBuilder(cmdline)
   129     if (cwd != null) proc.directory(cwd)
   130     if (env != null) {
   131       proc.environment.clear
   132       for ((x, y) <- env) proc.environment.put(x, y)
   133     }
   134     proc.redirectErrorStream(redirect)
   135     proc.start
   136   }
   137 
   138   def process_output(proc: Process): (String, Int) =
   139   {
   140     proc.getOutputStream.close
   141     val output = Source.fromInputStream(proc.getInputStream)(codec()).mkString  // FIXME
   142     val rc =
   143       try { proc.waitFor }
   144       finally {
   145         proc.getInputStream.close
   146         proc.getErrorStream.close
   147         proc.destroy
   148         Thread.interrupted
   149       }
   150     (output, rc)
   151   }
   152 
   153   def raw_exec(cwd: File, env: Map[String, String], redirect: Boolean, args: String*)
   154     : (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*))
   155 }
   156 
   157 
   158 class Standard_System
   159 {
   160   val platform_root = if (Platform.is_windows) Cygwin.check_root() else "/"
   161   override def toString = platform_root
   162 
   163 
   164   /* jvm_path */
   165 
   166   private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
   167   private val Named_Root = new Regex("//+([^/]*)(.*)")
   168 
   169   def jvm_path(posix_path: String): String =
   170     if (Platform.is_windows) {
   171       val result_path = new StringBuilder
   172       val rest =
   173         posix_path match {
   174           case Cygdrive(drive, rest) =>
   175             result_path ++= (drive + ":" + File.separator)
   176             rest
   177           case Named_Root(root, rest) =>
   178             result_path ++= File.separator
   179             result_path ++= File.separator
   180             result_path ++= root
   181             rest
   182           case path if path.startsWith("/") =>
   183             result_path ++= platform_root
   184             path
   185           case path => path
   186         }
   187       for (p <- rest.split("/") if p != "") {
   188         val len = result_path.length
   189         if (len > 0 && result_path(len - 1) != File.separatorChar)
   190           result_path += File.separatorChar
   191         result_path ++= p
   192       }
   193       result_path.toString
   194     }
   195     else posix_path
   196 
   197 
   198   /* posix_path */
   199 
   200   private val Platform_Root = new Regex("(?i)" +
   201     Pattern.quote(platform_root) + """(?:\\+|\z)(.*)""")
   202 
   203   private val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
   204 
   205   def posix_path(jvm_path: String): String =
   206     if (Platform.is_windows) {
   207       jvm_path.replace('/', '\\') match {
   208         case Platform_Root(rest) => "/" + rest.replace('\\', '/')
   209         case Drive(letter, rest) =>
   210           "/cygdrive/" + letter.toLowerCase(Locale.ENGLISH) +
   211             (if (rest == "") "" else "/" + rest.replace('\\', '/'))
   212         case path => path.replace('\\', '/')
   213       }
   214     }
   215     else jvm_path
   216 
   217 
   218   /* this_java executable */
   219 
   220   def this_java(): String =
   221   {
   222     val java_home = System.getProperty("java.home")
   223     val java_exe =
   224       if (Platform.is_windows) new File(java_home + "\\bin\\java.exe")
   225       else new File(java_home + "/bin/java")
   226     if (!java_exe.isFile) error("Expected this Java executable: " + java_exe.toString)
   227     posix_path(java_exe.getAbsolutePath)
   228   }
   229 }