src/Pure/System/standard_system.scala
author wenzelm
Thu Aug 02 12:36:54 2012 +0200 (2012-08-02)
changeset 48646 91281e9472d8
parent 48411 5b3440850d36
child 50203 00d8ad713e32
permissions -rw-r--r--
more official command specifications, including source position;
     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.regex.Pattern
    12 import java.util.Locale
    13 import java.net.URL
    14 import java.io.{File => JFile}
    15 import java.nio.charset.Charset
    16 
    17 import scala.io.Codec
    18 import scala.util.matching.Regex
    19 
    20 
    21 object Standard_System
    22 {
    23   /* UTF-8 charset */
    24 
    25   val charset_name: String = "UTF-8"
    26   val charset: Charset = Charset.forName(charset_name)
    27   def codec(): Codec = Codec(charset)
    28 
    29   def string_bytes(s: String): Array[Byte] = s.getBytes(charset)
    30 
    31 
    32   /* permissive UTF-8 decoding */
    33 
    34   // see also http://en.wikipedia.org/wiki/UTF-8#Description
    35   // overlong encodings enable byte-stuffing
    36 
    37   def decode_permissive_utf8(text: CharSequence): String =
    38   {
    39     val buf = new java.lang.StringBuilder(text.length)
    40     var code = -1
    41     var rest = 0
    42     def flush()
    43     {
    44       if (code != -1) {
    45         if (rest == 0 && Character.isValidCodePoint(code))
    46           buf.appendCodePoint(code)
    47         else buf.append('\uFFFD')
    48         code = -1
    49         rest = 0
    50       }
    51     }
    52     def init(x: Int, n: Int)
    53     {
    54       flush()
    55       code = x
    56       rest = n
    57     }
    58     def push(x: Int)
    59     {
    60       if (rest <= 0) init(x, -1)
    61       else {
    62         code <<= 6
    63         code += x
    64         rest -= 1
    65       }
    66     }
    67     for (i <- 0 until text.length) {
    68       val c = text.charAt(i)
    69       if (c < 128) { flush(); buf.append(c) }
    70       else if ((c & 0xC0) == 0x80) push(c & 0x3F)
    71       else if ((c & 0xE0) == 0xC0) init(c & 0x1F, 1)
    72       else if ((c & 0xF0) == 0xE0) init(c & 0x0F, 2)
    73       else if ((c & 0xF8) == 0xF0) init(c & 0x07, 3)
    74     }
    75     flush()
    76     buf.toString
    77   }
    78 
    79   private class Decode_Chars(decode: String => String,
    80     buffer: Array[Byte], start: Int, end: Int) extends CharSequence
    81   {
    82     def length: Int = end - start
    83     def charAt(i: Int): Char = (buffer(start + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
    84     def subSequence(i: Int, j: Int): CharSequence =
    85       new Decode_Chars(decode, buffer, start + i, start + j)
    86 
    87     // toString with adhoc decoding: abuse of CharSequence interface
    88     override def toString: String = decode(decode_permissive_utf8(this))
    89   }
    90 
    91   def decode_chars(decode: String => String,
    92     buffer: Array[Byte], start: Int, end: Int): CharSequence =
    93   {
    94     require(0 <= start && start <= end && end <= buffer.length)
    95     new Decode_Chars(decode, buffer, start, end)
    96   }
    97 
    98 
    99   /* shell processes */
   100 
   101   def raw_execute(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
   102   {
   103     val cmdline = new java.util.LinkedList[String]
   104     for (s <- args) cmdline.add(s)
   105 
   106     val proc = new ProcessBuilder(cmdline)
   107     if (cwd != null) proc.directory(cwd)
   108     if (env != null) {
   109       proc.environment.clear
   110       for ((x, y) <- env) proc.environment.put(x, y)
   111     }
   112     proc.redirectErrorStream(redirect)
   113     proc.start
   114   }
   115 
   116   def process_output(proc: Process): (String, Int) =
   117   {
   118     proc.getOutputStream.close
   119     val output = File.read(proc.getInputStream)
   120     val rc =
   121       try { proc.waitFor }
   122       finally {
   123         proc.getInputStream.close
   124         proc.getErrorStream.close
   125         proc.destroy
   126         Thread.interrupted
   127       }
   128     (output, rc)
   129   }
   130 
   131   def raw_exec(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
   132     : (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*))
   133 
   134 
   135   /* cygwin_root */
   136 
   137   def cygwin_root(): String =
   138   {
   139     val cygwin_root1 = System.getenv("CYGWIN_ROOT")
   140     val cygwin_root2 = System.getProperty("cygwin.root")
   141     val root =
   142       if (cygwin_root1 != null && cygwin_root1 != "") cygwin_root1
   143       else if (cygwin_root2 != null && cygwin_root2 != "") cygwin_root2
   144       else error("Bad Cygwin installation: unknown root")
   145 
   146     val root_file = new JFile(root)
   147     if (!new JFile(root_file, "bin\\bash.exe").isFile ||
   148         !new JFile(root_file, "bin\\env.exe").isFile ||
   149         !new JFile(root_file, "bin\\tar.exe").isFile)
   150       error("Bad Cygwin installation: " + quote(root))
   151 
   152     root
   153   }
   154 }
   155 
   156 
   157 class Standard_System
   158 {
   159   /* platform_root */
   160 
   161   val platform_root = if (Platform.is_windows) Standard_System.cygwin_root() else "/"
   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.toUpperCase(Locale.ENGLISH) + ":" + JFile.separator)
   176             rest
   177           case Named_Root(root, rest) =>
   178             result_path ++= JFile.separator
   179             result_path ++= JFile.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 <- space_explode('/', rest) if p != "") {
   188         val len = result_path.length
   189         if (len > 0 && result_path(len - 1) != JFile.separatorChar)
   190           result_path += JFile.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   /* JDK home of running JVM */
   219 
   220   def this_jdk_home(): String =
   221   {
   222     val java_home = System.getProperty("java.home")
   223     val home = new JFile(java_home)
   224     val parent = home.getParent
   225     val jdk_home =
   226       if (home.getName == "jre" && parent != null &&
   227           (new JFile(new JFile(parent, "bin"), "javac")).exists) parent
   228       else java_home
   229     posix_path(jdk_home)
   230   }
   231 }