# HG changeset patch
# User wenzelm
# Date 1219316737 -7200
# Node ID 947cb8e3d3139737b09683a3d7d047cee47e6ca0
# Parent  68d40072e9e706db33e1a5a4ba0b262c389b4416
added get_setting;
removed obsolete ISABELLE_HOME, ISABELLE_HOME_USER;
added platform_path, which expands variables and performs basic cygwin conversion;

diff -r 68d40072e9e7 -r 947cb8e3d313 src/Pure/Tools/isabelle_system.scala
--- a/src/Pure/Tools/isabelle_system.scala	Thu Aug 21 13:05:31 2008 +0200
+++ b/src/Pure/Tools/isabelle_system.scala	Thu Aug 21 13:05:37 2008 +0200
@@ -2,11 +2,14 @@
     ID:         $Id$
     Author:     Makarius
 
-Isabelle system support.
+Isabelle system support: settings and path specifications.
 */
 
 package isabelle
 
+import java.util.regex.{Pattern, Matcher}
+import java.io.File
+
 
 object IsabelleSystem {
 
@@ -14,13 +17,52 @@
 
   class BadSetting(val name: String) extends Exception
 
-  private def strict_getenv(name: String) = {
+  def get_setting(name: String) = {
     val value = System.getenv(name)
     if (value == null || value == "") throw new BadSetting(name)
     else value
   }
 
-  def ISABELLE_HOME() = strict_getenv("ISABELLE_HOME_JVM")
-  def ISABELLE_HOME_USER() = strict_getenv("ISABELLE_HOME_USER_JVM")
+
+  /* File path specifications */
+
+  private val cygdrive_pattern = Pattern.compile("/cygdrive/([a-zA-Z])($|/.*)")
+
+  def platform_path(source_path: String) = {
+    val result_path = new StringBuilder
 
+    def init(path: String) = {
+      val cygdrive = cygdrive_pattern.matcher(path)
+      if (cygdrive.matches) {
+        result_path.setLength(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"))
+        path.substring(1)
+      }
+      else path
+    }
+    def append(path: String) = {
+      for (p <- init(path).split("/")) {
+        if (p != "") {
+          val len = result_path.length
+          if (len > 0 && result_path(len - 1) != File.separatorChar)
+            result_path.append(File.separator)
+          result_path.append(p)
+        }
+      }
+    }
+    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"))
+      else append(p)
+    }
+    result_path.toString
+  }
 }