src/Pure/System/standard_system.scala
author wenzelm
Fri Jul 20 22:29:25 2012 +0200 (2012-07-20)
changeset 48409 0d2114eb412a
parent 48373 527e2bad7cca
child 48411 5b3440850d36
permissions -rw-r--r--
more explicit java.io.{File => JFile};
     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.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
    15   BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader,
    16   File => JFile, FileFilter, IOException}
    17 import java.nio.charset.Charset
    18 import java.util.zip.GZIPOutputStream
    19 
    20 import scala.io.Codec
    21 import scala.util.matching.Regex
    22 import scala.collection.mutable
    23 
    24 
    25 object Standard_System
    26 {
    27   /* UTF-8 charset */
    28 
    29   val charset_name: String = "UTF-8"
    30   val charset: Charset = Charset.forName(charset_name)
    31   def codec(): Codec = Codec(charset)
    32 
    33   def string_bytes(s: String): Array[Byte] = s.getBytes(charset)
    34 
    35 
    36   /* permissive UTF-8 decoding */
    37 
    38   // see also http://en.wikipedia.org/wiki/UTF-8#Description
    39   // overlong encodings enable byte-stuffing
    40 
    41   def decode_permissive_utf8(text: CharSequence): String =
    42   {
    43     val buf = new java.lang.StringBuilder(text.length)
    44     var code = -1
    45     var rest = 0
    46     def flush()
    47     {
    48       if (code != -1) {
    49         if (rest == 0 && Character.isValidCodePoint(code))
    50           buf.appendCodePoint(code)
    51         else buf.append('\uFFFD')
    52         code = -1
    53         rest = 0
    54       }
    55     }
    56     def init(x: Int, n: Int)
    57     {
    58       flush()
    59       code = x
    60       rest = n
    61     }
    62     def push(x: Int)
    63     {
    64       if (rest <= 0) init(x, -1)
    65       else {
    66         code <<= 6
    67         code += x
    68         rest -= 1
    69       }
    70     }
    71     for (i <- 0 until text.length) {
    72       val c = text.charAt(i)
    73       if (c < 128) { flush(); buf.append(c) }
    74       else if ((c & 0xC0) == 0x80) push(c & 0x3F)
    75       else if ((c & 0xE0) == 0xC0) init(c & 0x1F, 1)
    76       else if ((c & 0xF0) == 0xE0) init(c & 0x0F, 2)
    77       else if ((c & 0xF8) == 0xF0) init(c & 0x07, 3)
    78     }
    79     flush()
    80     buf.toString
    81   }
    82 
    83   private class Decode_Chars(decode: String => String,
    84     buffer: Array[Byte], start: Int, end: Int) extends CharSequence
    85   {
    86     def length: Int = end - start
    87     def charAt(i: Int): Char = (buffer(start + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
    88     def subSequence(i: Int, j: Int): CharSequence =
    89       new Decode_Chars(decode, buffer, start + i, start + j)
    90 
    91     // toString with adhoc decoding: abuse of CharSequence interface
    92     override def toString: String = decode(decode_permissive_utf8(this))
    93   }
    94 
    95   def decode_chars(decode: String => String,
    96     buffer: Array[Byte], start: Int, end: Int): CharSequence =
    97   {
    98     require(0 <= start && start <= end && end <= buffer.length)
    99     new Decode_Chars(decode, buffer, start, end)
   100   }
   101 
   102 
   103   /* basic file operations */
   104 
   105   def slurp(reader: BufferedReader): String =
   106   {
   107     val output = new StringBuilder(100)
   108     var c = -1
   109     while ({ c = reader.read; c != -1 }) output += c.toChar
   110     reader.close
   111     output.toString
   112   }
   113 
   114   def slurp(stream: InputStream): String =
   115     slurp(new BufferedReader(new InputStreamReader(stream, charset)))
   116 
   117   def read_file(file: JFile): String = slurp(new FileInputStream(file))
   118 
   119   def write_file(file: JFile, text: CharSequence, zip: Boolean = false)
   120   {
   121     val stream1 = new FileOutputStream(file)
   122     val stream2 = if (zip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1
   123     val writer = new BufferedWriter(new OutputStreamWriter(stream2, charset))
   124     try { writer.append(text) }
   125     finally { writer.close }
   126   }
   127 
   128   def eq_file(file1: JFile, file2: JFile): Boolean =
   129     file1.getCanonicalPath == file2.getCanonicalPath  // FIXME prefer java.nio.file.Files.isSameFile of Java 1.7
   130 
   131   def copy_file(src: JFile, dst: JFile) =
   132     if (!eq_file(src, dst)) {
   133       val in = new FileInputStream(src)
   134       try {
   135         val out = new FileOutputStream(dst)
   136         try {
   137           val buf = new Array[Byte](65536)
   138           var m = 0
   139           do {
   140             m = in.read(buf, 0, buf.length)
   141             if (m != -1) out.write(buf, 0, m)
   142           } while (m != -1)
   143         }
   144         finally { out.close }
   145       }
   146       finally { in.close }
   147     }
   148 
   149   def with_tmp_file[A](prefix: String)(body: JFile => A): A =
   150   {
   151     val file = JFile.createTempFile(prefix, null)
   152     file.deleteOnExit
   153     try { body(file) } finally { file.delete }
   154   }
   155 
   156   // FIXME handle (potentially cyclic) directory graph
   157   def find_files(start: JFile, ok: JFile => Boolean): List[JFile] =
   158   {
   159     val files = new mutable.ListBuffer[JFile]
   160     val filter = new FileFilter { def accept(entry: JFile) = entry.isDirectory || ok(entry) }
   161     def find_entry(entry: JFile)
   162     {
   163       if (ok(entry)) files += entry
   164       if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry)
   165     }
   166     find_entry(start)
   167     files.toList
   168   }
   169 
   170 
   171   /* shell processes */
   172 
   173   def raw_execute(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
   174   {
   175     val cmdline = new java.util.LinkedList[String]
   176     for (s <- args) cmdline.add(s)
   177 
   178     val proc = new ProcessBuilder(cmdline)
   179     if (cwd != null) proc.directory(cwd)
   180     if (env != null) {
   181       proc.environment.clear
   182       for ((x, y) <- env) proc.environment.put(x, y)
   183     }
   184     proc.redirectErrorStream(redirect)
   185     proc.start
   186   }
   187 
   188   def process_output(proc: Process): (String, Int) =
   189   {
   190     proc.getOutputStream.close
   191     val output = slurp(proc.getInputStream)
   192     val rc =
   193       try { proc.waitFor }
   194       finally {
   195         proc.getInputStream.close
   196         proc.getErrorStream.close
   197         proc.destroy
   198         Thread.interrupted
   199       }
   200     (output, rc)
   201   }
   202 
   203   def raw_exec(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
   204     : (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*))
   205 
   206 
   207   /* cygwin_root */
   208 
   209   def cygwin_root(): String =
   210   {
   211     val cygwin_root1 = System.getenv("CYGWIN_ROOT")
   212     val cygwin_root2 = System.getProperty("cygwin.root")
   213     val root =
   214       if (cygwin_root1 != null && cygwin_root1 != "") cygwin_root1
   215       else if (cygwin_root2 != null && cygwin_root2 != "") cygwin_root2
   216       else error("Bad Cygwin installation: unknown root")
   217 
   218     val root_file = new JFile(root)
   219     if (!new JFile(root_file, "bin\\bash.exe").isFile ||
   220         !new JFile(root_file, "bin\\env.exe").isFile ||
   221         !new JFile(root_file, "bin\\tar.exe").isFile)
   222       error("Bad Cygwin installation: " + quote(root))
   223 
   224     root
   225   }
   226 }
   227 
   228 
   229 class Standard_System
   230 {
   231   /* platform_root */
   232 
   233   val platform_root = if (Platform.is_windows) Standard_System.cygwin_root() else "/"
   234 
   235 
   236   /* jvm_path */
   237 
   238   private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
   239   private val Named_Root = new Regex("//+([^/]*)(.*)")
   240 
   241   def jvm_path(posix_path: String): String =
   242     if (Platform.is_windows) {
   243       val result_path = new StringBuilder
   244       val rest =
   245         posix_path match {
   246           case Cygdrive(drive, rest) =>
   247             result_path ++= (drive.toUpperCase(Locale.ENGLISH) + ":" + JFile.separator)
   248             rest
   249           case Named_Root(root, rest) =>
   250             result_path ++= JFile.separator
   251             result_path ++= JFile.separator
   252             result_path ++= root
   253             rest
   254           case path if path.startsWith("/") =>
   255             result_path ++= platform_root
   256             path
   257           case path => path
   258         }
   259       for (p <- space_explode('/', rest) if p != "") {
   260         val len = result_path.length
   261         if (len > 0 && result_path(len - 1) != JFile.separatorChar)
   262           result_path += JFile.separatorChar
   263         result_path ++= p
   264       }
   265       result_path.toString
   266     }
   267     else posix_path
   268 
   269 
   270   /* posix_path */
   271 
   272   private val Platform_Root = new Regex("(?i)" +
   273     Pattern.quote(platform_root) + """(?:\\+|\z)(.*)""")
   274 
   275   private val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
   276 
   277   def posix_path(jvm_path: String): String =
   278     if (Platform.is_windows) {
   279       jvm_path.replace('/', '\\') match {
   280         case Platform_Root(rest) => "/" + rest.replace('\\', '/')
   281         case Drive(letter, rest) =>
   282           "/cygdrive/" + letter.toLowerCase(Locale.ENGLISH) +
   283             (if (rest == "") "" else "/" + rest.replace('\\', '/'))
   284         case path => path.replace('\\', '/')
   285       }
   286     }
   287     else jvm_path
   288 
   289 
   290   /* JDK home of running JVM */
   291 
   292   def this_jdk_home(): String =
   293   {
   294     val java_home = System.getProperty("java.home")
   295     val home = new JFile(java_home)
   296     val parent = home.getParent
   297     val jdk_home =
   298       if (home.getName == "jre" && parent != null &&
   299           (new JFile(new JFile(parent, "bin"), "javac")).exists) parent
   300       else java_home
   301     posix_path(jdk_home)
   302   }
   303 }