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