more precise treatment of UNC server prefix, e.g. //foo;
authorwenzelm
Wed Apr 14 22:08:47 2010 +0200 (2010-04-14 ago)
changeset 3613689b1a136edef
parent 36135 89d1903fbd50
child 36145 42d690c1cd31
more precise treatment of UNC server prefix, e.g. //foo;
src/Pure/System/isabelle_system.scala
src/Pure/System/standard_system.scala
     1.1 --- a/src/Pure/System/isabelle_system.scala	Wed Apr 14 22:07:01 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_system.scala	Wed Apr 14 22:08:47 2010 +0200
     1.3 @@ -88,31 +88,39 @@
     1.4  
     1.5    /* expand_path */
     1.6  
     1.7 +  private val Root = new Regex("(//+[^/]*|/)(.*)")
     1.8 +  private val Only_Root = new Regex("//+[^/]*|/")
     1.9 +
    1.10    def expand_path(isabelle_path: String): String =
    1.11    {
    1.12      val result_path = new StringBuilder
    1.13 -    def init(path: String)
    1.14 +    def init(path: String): String =
    1.15      {
    1.16 -      if (path.startsWith("/")) {
    1.17 -        result_path.clear
    1.18 -        result_path += '/'
    1.19 +      path match {
    1.20 +        case Root(root, rest) =>
    1.21 +          result_path.clear
    1.22 +          result_path ++= root
    1.23 +          rest
    1.24 +        case _ => path
    1.25        }
    1.26      }
    1.27      def append(path: String)
    1.28      {
    1.29 -      init(path)
    1.30 -      for (p <- path.split("/") if p != "" && p != ".") {
    1.31 +      val rest = init(path)
    1.32 +      for (p <- rest.split("/") if p != "" && p != ".") {
    1.33          if (p == "..") {
    1.34            val result = result_path.toString
    1.35 -          val i = result.lastIndexOf("/")
    1.36 -          if (result == "")
    1.37 -            result_path ++= ".."
    1.38 -          else if (result.substring(i + 1) == "..")
    1.39 -            result_path ++= "/.."
    1.40 -          else if (i < 1)
    1.41 -            result_path.length = i + 1
    1.42 -          else
    1.43 -            result_path.length = i
    1.44 +          if (!Only_Root.pattern.matcher(result).matches) {
    1.45 +            val i = result.lastIndexOf("/")
    1.46 +            if (result == "")
    1.47 +              result_path ++= ".."
    1.48 +            else if (result.substring(i + 1) == "..")
    1.49 +              result_path ++= "/.."
    1.50 +            else if (i < 0)
    1.51 +              result_path.length = 0
    1.52 +            else
    1.53 +              result_path.length = i
    1.54 +          }
    1.55          }
    1.56          else {
    1.57            val len = result_path.length
    1.58 @@ -122,8 +130,8 @@
    1.59          }
    1.60        }
    1.61      }
    1.62 -    init(isabelle_path)
    1.63 -    for (p <- isabelle_path.split("/")) {
    1.64 +    val rest = init(isabelle_path)
    1.65 +    for (p <- rest.split("/")) {
    1.66        if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
    1.67        else if (p == "~") append(getenv_strict("HOME"))
    1.68        else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
     2.1 --- a/src/Pure/System/standard_system.scala	Wed Apr 14 22:07:01 2010 +0200
     2.2 +++ b/src/Pure/System/standard_system.scala	Wed Apr 14 22:08:47 2010 +0200
     2.3 @@ -162,6 +162,7 @@
     2.4    /* jvm_path */
     2.5  
     2.6    private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
     2.7 +  private val Named_Root = new Regex("//+([^/]*)(.*)")
     2.8  
     2.9    def jvm_path(posix_path: String): String =
    2.10      if (Platform.is_windows) {
    2.11 @@ -171,6 +172,11 @@
    2.12            case Cygdrive(drive, rest) =>
    2.13              result_path ++= (drive + ":" + File.separator)
    2.14              rest
    2.15 +          case Named_Root(root, rest) =>
    2.16 +            result_path ++= File.separator
    2.17 +            result_path ++= File.separator
    2.18 +            result_path ++= root
    2.19 +            rest
    2.20            case path if path.startsWith("/") =>
    2.21              result_path ++= platform_root
    2.22              path