1.1 --- a/src/Pure/Tools/isabelle_system.scala	Thu Aug 21 13:05:31 2008 +0200
     1.2 +++ b/src/Pure/Tools/isabelle_system.scala	Thu Aug 21 13:05:37 2008 +0200
     1.3 @@ -2,11 +2,14 @@
     1.4      ID:         $Id$
     1.5      Author:     Makarius
     1.6  
     1.7 -Isabelle system support.
     1.8 +Isabelle system support: settings and path specifications.
     1.9  */
    1.10  
    1.11  package isabelle
    1.12  
    1.13 +import java.util.regex.{Pattern, Matcher}
    1.14 +import java.io.File
    1.15 +
    1.16  
    1.17  object IsabelleSystem {
    1.18  
    1.19 @@ -14,13 +17,52 @@
    1.20  
    1.21    class BadSetting(val name: String) extends Exception
    1.22  
    1.23 -  private def strict_getenv(name: String) = {
    1.24 +  def get_setting(name: String) = {
    1.25      val value = System.getenv(name)
    1.26      if (value == null || value == "") throw new BadSetting(name)
    1.27      else value
    1.28    }
    1.29  
    1.30 -  def ISABELLE_HOME() = strict_getenv("ISABELLE_HOME_JVM")
    1.31 -  def ISABELLE_HOME_USER() = strict_getenv("ISABELLE_HOME_USER_JVM")
    1.32  
    1.33 +  /* File path specifications */
    1.34 +
    1.35 +  private val cygdrive_pattern = Pattern.compile("/cygdrive/([a-zA-Z])($|/.*)")
    1.36 +
    1.37 +  def platform_path(source_path: String) = {
    1.38 +    val result_path = new StringBuilder
    1.39 +
    1.40 +    def init(path: String) = {
    1.41 +      val cygdrive = cygdrive_pattern.matcher(path)
    1.42 +      if (cygdrive.matches) {
    1.43 +        result_path.setLength(0)
    1.44 +        result_path.append(cygdrive.group(1))
    1.45 +        result_path.append(":")
    1.46 +        result_path.append(File.separator)
    1.47 +        cygdrive.group(2)
    1.48 +      }
    1.49 +      else if (path.startsWith("/")) {
    1.50 +        result_path.setLength(0)
    1.51 +        result_path.append(get_setting("ISABELLE_ROOT_JVM"))
    1.52 +        path.substring(1)
    1.53 +      }
    1.54 +      else path
    1.55 +    }
    1.56 +    def append(path: String) = {
    1.57 +      for (p <- init(path).split("/")) {
    1.58 +        if (p != "") {
    1.59 +          val len = result_path.length
    1.60 +          if (len > 0 && result_path(len - 1) != File.separatorChar)
    1.61 +            result_path.append(File.separator)
    1.62 +          result_path.append(p)
    1.63 +        }
    1.64 +      }
    1.65 +    }
    1.66 +    for (p <- init(source_path).split("/")) {
    1.67 +      if (p.startsWith("$")) append(get_setting(p.substring(1)))
    1.68 +      else if (p == "~") append(get_setting("HOME"))
    1.69 +      else if (p == "~~") append(get_setting("ISABELLE_HOME"))
    1.70 +      else append(p)
    1.71 +    }
    1.72 +    result_path.toString
    1.73 +  }
    1.74  }