src/Pure/Tools/isabelle_system.scala
author wenzelm
Sat Aug 23 23:07:46 2008 +0200 (2008-08-23)
changeset 27974 1dfb0e260e4c
parent 27962 28a306e675ba
child 27993 6dd90ef9f927
permissions -rw-r--r--
added exec;
private posix_prefix;
     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.File
    12 
    13 
    14 object IsabelleSystem {
    15 
    16   /* Isabelle settings */
    17 
    18   def getenv(name: String) = {
    19     val value = System.getenv(name)
    20     if (value != null) value else ""
    21   }
    22 
    23   class BadVariable(val name: String) extends Exception {
    24     override def toString = "BadVariable: " + name
    25   }
    26 
    27   def getenv_strict(name: String) = {
    28     val value = getenv(name)
    29     if (value != "") value else throw new BadVariable(name)
    30   }
    31 
    32 
    33   /* file path specifications */
    34 
    35   private val cygdrive_pattern = Pattern.compile("/cygdrive/([a-zA-Z])($|/.*)")
    36 
    37   def platform_path(source_path: String) = {
    38     val result_path = new StringBuilder
    39 
    40     def init(path: String) = {
    41       val cygdrive = cygdrive_pattern.matcher(path)
    42       if (cygdrive.matches) {
    43         result_path.length = 0
    44         result_path.append(cygdrive.group(1))
    45         result_path.append(":")
    46         result_path.append(File.separator)
    47         cygdrive.group(2)
    48       }
    49       else if (path.startsWith("/")) {
    50         result_path.length = 0
    51         result_path.append(getenv_strict("ISABELLE_ROOT_JVM"))
    52         path.substring(1)
    53       }
    54       else path
    55     }
    56     def append(path: String) = {
    57       for (p <- init(path).split("/")) {
    58         if (p != "") {
    59           val len = result_path.length
    60           if (len > 0 && result_path(len - 1) != File.separatorChar)
    61             result_path.append(File.separator)
    62           result_path.append(p)
    63         }
    64       }
    65     }
    66     for (p <- init(source_path).split("/")) {
    67       if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
    68       else if (p == "~") append(getenv_strict("HOME"))
    69       else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
    70       else append(p)
    71     }
    72     result_path.toString
    73   }
    74 
    75 
    76   /* processes */
    77 
    78   private def posix_prefix() = {
    79     if (Pattern.matches(".*-cygwin", getenv_strict("ML_PLATFORM")))
    80       List(platform_path("/bin/env"))
    81     else Nil
    82   }
    83 
    84   def exec(args: List[String]) = Runtime.getRuntime.exec((posix_prefix() ++ args).toArray)
    85 
    86 }