added getenv;
renamed get_setting to getenv_strict;
added shell_prefix (for Cygwin);
--- a/src/Pure/Tools/isabelle_system.scala Sat Aug 23 17:22:53 2008 +0200
+++ b/src/Pure/Tools/isabelle_system.scala Sat Aug 23 17:22:54 2008 +0200
@@ -15,12 +15,16 @@
/* Isabelle settings */
- class BadSetting(val name: String) extends Exception
+ def getenv(name: String) = {
+ val value = System.getenv(name)
+ if (value != null) value else ""
+ }
- def get_setting(name: String) = {
- val value = System.getenv(name)
- if (value == null || value == "") throw new BadSetting(name)
- else value
+ class BadVariable(val name: String) extends Exception
+
+ def getenv_strict(name: String) = {
+ val value = getenv(name)
+ if (value != "") value else throw new BadVariable(name)
}
@@ -34,15 +38,15 @@
def init(path: String) = {
val cygdrive = cygdrive_pattern.matcher(path)
if (cygdrive.matches) {
- result_path.setLength(0)
+ result_path.length = 0
result_path.append(cygdrive.group(1))
result_path.append(":")
result_path.append(File.separator)
cygdrive.group(2)
}
else if (path.startsWith("/")) {
- result_path.setLength(0)
- result_path.append(get_setting("ISABELLE_ROOT_JVM"))
+ result_path.length = 0
+ result_path.append(getenv_strict("ISABELLE_ROOT_JVM"))
path.substring(1)
}
else path
@@ -58,11 +62,21 @@
}
}
for (p <- init(source_path).split("/")) {
- if (p.startsWith("$")) append(get_setting(p.substring(1)))
- else if (p == "~") append(get_setting("HOME"))
- else if (p == "~~") append(get_setting("ISABELLE_HOME"))
+ if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
+ else if (p == "~") append(getenv_strict("HOME"))
+ else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
else append(p)
}
result_path.toString
}
+
+
+ /* Cygwin shell prefix */
+
+ def shell_prefix() = {
+ if (Pattern.matches(".*-cygwin", getenv_strict("ML_PLATFORM")))
+ Some(platform_path("/usr/bin/env"))
+ else None
+ }
+
}