src/Pure/Tools/isabelle_system.scala
author wenzelm
Sat Oct 04 16:05:09 2008 +0200 (2008-10-04 ago)
changeset 28500 4b79e5d3d0aa
parent 28496 4cff10648928
child 29140 e7ac5bb20aed
permissions -rw-r--r--
replaced ISATOOL by ISABELLE_TOOL;
     1 /*  Title:      Pure/Tools/isabelle_system.scala
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Isabelle system support -- basic Cygwin/Posix compatibility.
     6 */
     7 
     8 package isabelle
     9 
    10 import java.util.regex.{Pattern, Matcher}
    11 import java.io.{BufferedReader, InputStreamReader, FileInputStream, File, IOException}
    12 
    13 import scala.io.Source
    14 
    15 
    16 object IsabelleSystem {
    17 
    18   val charset = "UTF-8"
    19 
    20 
    21   /* Isabelle environment settings */
    22 
    23   def getenv(name: String) = {
    24     val value = System.getenv(if (name == "HOME") "HOME_JVM" else name)
    25     if (value != null) value else ""
    26   }
    27 
    28   def getenv_strict(name: String) = {
    29     val value = getenv(name)
    30     if (value != "") value else error("Undefined environment variable: " + name)
    31   }
    32 
    33   def is_cygwin() = Pattern.matches(".*-cygwin", getenv_strict("ML_PLATFORM"))
    34 
    35 
    36   /* file path specifications */
    37 
    38   private val cygdrive_pattern = Pattern.compile("/cygdrive/([a-zA-Z])($|/.*)")
    39 
    40   def platform_path(source_path: String) = {
    41     val result_path = new StringBuilder
    42 
    43     def init(path: String) = {
    44       val cygdrive = cygdrive_pattern.matcher(path)
    45       if (cygdrive.matches) {
    46         result_path.length = 0
    47         result_path.append(cygdrive.group(1))
    48         result_path.append(":")
    49         result_path.append(File.separator)
    50         cygdrive.group(2)
    51       }
    52       else if (path.startsWith("/")) {
    53         result_path.length = 0
    54         result_path.append(getenv_strict("ISABELLE_ROOT_JVM"))
    55         path.substring(1)
    56       }
    57       else path
    58     }
    59     def append(path: String) = {
    60       for (p <- init(path).split("/")) {
    61         if (p != "") {
    62           val len = result_path.length
    63           if (len > 0 && result_path(len - 1) != File.separatorChar)
    64             result_path.append(File.separator)
    65           result_path.append(p)
    66         }
    67       }
    68     }
    69     for (p <- init(source_path).split("/")) {
    70       if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
    71       else if (p == "~") append(getenv_strict("HOME"))
    72       else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
    73       else append(p)
    74     }
    75     result_path.toString
    76   }
    77 
    78 
    79   /* processes */
    80 
    81   private def posix_prefix() = if (is_cygwin()) List(platform_path("/bin/env")) else Nil
    82 
    83   def exec(args: String*): Process = Runtime.getRuntime.exec((posix_prefix() ++ args).toArray)
    84 
    85   def exec2(args: String*): Process = {
    86     val cmdline = new java.util.LinkedList[String]
    87     for (s <- posix_prefix() ++ args) cmdline.add(s)
    88     new ProcessBuilder(cmdline).redirectErrorStream(true).start
    89   }
    90 
    91 
    92   /* Isabelle tools (non-interactive) */
    93 
    94   def isabelle_tool(args: String*) = {
    95     val proc =
    96       try { exec2((List(getenv_strict("ISABELLE_TOOL")) ++ args): _*) }
    97       catch { case e: IOException => error(e.getMessage) }
    98     proc.getOutputStream.close
    99     val output = Source.fromInputStream(proc.getInputStream, charset).mkString("")
   100     val rc = proc.waitFor
   101     (output, rc)
   102   }
   103 
   104 
   105   /* named pipes */
   106 
   107   def mk_fifo() = {
   108     val (result, rc) = isabelle_tool("mkfifo")
   109     if (rc == 0) result.trim
   110     else error(result)
   111   }
   112 
   113   def rm_fifo(fifo: String) = {
   114     val (result, rc) = isabelle_tool("rmfifo", fifo)
   115     if (rc != 0) error(result)
   116   }
   117 
   118   def fifo_reader(fifo: String) =  // blocks until writer is ready
   119     if (is_cygwin()) new BufferedReader(new InputStreamReader(Runtime.getRuntime.exec(
   120       Array(platform_path("/bin/cat"), fifo)).getInputStream, charset))
   121     else new BufferedReader(new InputStreamReader(new FileInputStream(fifo), charset))
   122 
   123 }