# HG changeset patch
# User wenzelm
# Date 1219504974 -7200
# Node ID b2003c98897ccc91e345ce0163dfa5ab39de9d21
# Parent  0576c91a68034ad7f47657ea566da6be1786aae3
added getenv;
renamed get_setting to getenv_strict;
added shell_prefix (for Cygwin);

diff -r 0576c91a6803 -r b2003c98897c src/Pure/Tools/isabelle_system.scala
--- 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
+  }
+
 }