src/Pure/Tools/isabelle_system.scala
changeset 27953 b2003c98897c
parent 27936 947cb8e3d313
child 27956 84bfb2162dd2
equal deleted inserted replaced
27952:0576c91a6803 27953:b2003c98897c
    13 
    13 
    14 object IsabelleSystem {
    14 object IsabelleSystem {
    15 
    15 
    16   /* Isabelle settings */
    16   /* Isabelle settings */
    17 
    17 
    18   class BadSetting(val name: String) extends Exception
    18   def getenv(name: String) = {
       
    19     val value = System.getenv(name)
       
    20     if (value != null) value else ""
       
    21   }
    19 
    22 
    20   def get_setting(name: String) = {
    23   class BadVariable(val name: String) extends Exception
    21     val value = System.getenv(name)
    24 
    22     if (value == null || value == "") throw new BadSetting(name)
    25   def getenv_strict(name: String) = {
    23     else value
    26     val value = getenv(name)
       
    27     if (value != "") value else throw new BadVariable(name)
    24   }
    28   }
    25 
    29 
    26 
    30 
    27   /* File path specifications */
    31   /* File path specifications */
    28 
    32 
    32     val result_path = new StringBuilder
    36     val result_path = new StringBuilder
    33 
    37 
    34     def init(path: String) = {
    38     def init(path: String) = {
    35       val cygdrive = cygdrive_pattern.matcher(path)
    39       val cygdrive = cygdrive_pattern.matcher(path)
    36       if (cygdrive.matches) {
    40       if (cygdrive.matches) {
    37         result_path.setLength(0)
    41         result_path.length = 0
    38         result_path.append(cygdrive.group(1))
    42         result_path.append(cygdrive.group(1))
    39         result_path.append(":")
    43         result_path.append(":")
    40         result_path.append(File.separator)
    44         result_path.append(File.separator)
    41         cygdrive.group(2)
    45         cygdrive.group(2)
    42       }
    46       }
    43       else if (path.startsWith("/")) {
    47       else if (path.startsWith("/")) {
    44         result_path.setLength(0)
    48         result_path.length = 0
    45         result_path.append(get_setting("ISABELLE_ROOT_JVM"))
    49         result_path.append(getenv_strict("ISABELLE_ROOT_JVM"))
    46         path.substring(1)
    50         path.substring(1)
    47       }
    51       }
    48       else path
    52       else path
    49     }
    53     }
    50     def append(path: String) = {
    54     def append(path: String) = {
    56           result_path.append(p)
    60           result_path.append(p)
    57         }
    61         }
    58       }
    62       }
    59     }
    63     }
    60     for (p <- init(source_path).split("/")) {
    64     for (p <- init(source_path).split("/")) {
    61       if (p.startsWith("$")) append(get_setting(p.substring(1)))
    65       if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
    62       else if (p == "~") append(get_setting("HOME"))
    66       else if (p == "~") append(getenv_strict("HOME"))
    63       else if (p == "~~") append(get_setting("ISABELLE_HOME"))
    67       else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
    64       else append(p)
    68       else append(p)
    65     }
    69     }
    66     result_path.toString
    70     result_path.toString
    67   }
    71   }
       
    72 
       
    73 
       
    74   /* Cygwin shell prefix */
       
    75 
       
    76   def shell_prefix() = {
       
    77     if (Pattern.matches(".*-cygwin", getenv_strict("ML_PLATFORM")))
       
    78       Some(platform_path("/usr/bin/env"))
       
    79     else None
       
    80   }
       
    81 
    68 }
    82 }