src/Pure/System/standard_system.scala
author wenzelm
Tue Aug 10 18:24:16 2010 +0200 (2010-08-10)
changeset 38264 205b74a1bb18
parent 36193 067a01827fca
child 39522 01aade784da9
permissions -rw-r--r--
added string_bytes convenience;
     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 
   136     try { proc.start }
   137     catch { case e: IOException => error(e.getMessage) }
   138   }
   139 
   140   def process_output(proc: Process): (String, Int) =
   141   {
   142     proc.getOutputStream.close
   143     val output = Source.fromInputStream(proc.getInputStream)(codec()).mkString  // FIXME
   144     val rc =
   145       try { proc.waitFor }
   146       finally {
   147         proc.getInputStream.close
   148         proc.getErrorStream.close
   149         proc.destroy
   150         Thread.interrupted
   151       }
   152     (output, rc)
   153   }
   154 
   155   def raw_exec(cwd: File, env: Map[String, String], redirect: Boolean, args: String*):
   156     (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*))
   157 }
   158 
   159 
   160 class Standard_System
   161 {
   162   val platform_root = if (Platform.is_windows) Cygwin.check_root() else "/"
   163   override def toString = platform_root
   164 
   165 
   166   /* jvm_path */
   167 
   168   private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
   169   private val Named_Root = new Regex("//+([^/]*)(.*)")
   170 
   171   def jvm_path(posix_path: String): String =
   172     if (Platform.is_windows) {
   173       val result_path = new StringBuilder
   174       val rest =
   175         posix_path match {
   176           case Cygdrive(drive, rest) =>
   177             result_path ++= (drive + ":" + File.separator)
   178             rest
   179           case Named_Root(root, rest) =>
   180             result_path ++= File.separator
   181             result_path ++= File.separator
   182             result_path ++= root
   183             rest
   184           case path if path.startsWith("/") =>
   185             result_path ++= platform_root
   186             path
   187           case path => path
   188         }
   189       for (p <- rest.split("/") if p != "") {
   190         val len = result_path.length
   191         if (len > 0 && result_path(len - 1) != File.separatorChar)
   192           result_path += File.separatorChar
   193         result_path ++= p
   194       }
   195       result_path.toString
   196     }
   197     else posix_path
   198 
   199 
   200   /* posix_path */
   201 
   202   private val Platform_Root = new Regex("(?i)" +
   203     Pattern.quote(platform_root) + """(?:\\+|\z)(.*)""")
   204 
   205   private val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
   206 
   207   def posix_path(jvm_path: String): String =
   208     if (Platform.is_windows) {
   209       jvm_path.replace('/', '\\') match {
   210         case Platform_Root(rest) => "/" + rest.replace('\\', '/')
   211         case Drive(letter, rest) =>
   212           "/cygdrive/" + letter.toLowerCase(Locale.ENGLISH) +
   213             (if (rest == "") "" else "/" + rest.replace('\\', '/'))
   214         case path => path.replace('\\', '/')
   215       }
   216     }
   217     else jvm_path
   218 
   219 
   220   /* this_java executable */
   221 
   222   def this_java(): String =
   223   {
   224     val java_home = System.getProperty("java.home")
   225     val java_exe =
   226       if (Platform.is_windows) new File(java_home + "\\bin\\java.exe")
   227       else new File(java_home + "/bin/java")
   228     if (!java_exe.isFile) error("Expected this Java executable: " + java_exe.toString)
   229     posix_path(java_exe.getAbsolutePath)
   230   }
   231 }