# HG changeset patch
# User wenzelm
# Date 1271275727 -7200
# Node ID 89b1a136edef1ddb940fc9fa45bd9db537c8743a
# Parent  89d1903fbd50f34f9676e01f6b34202e74c8cda8
more precise treatment of UNC server prefix, e.g. //foo;

diff -r 89d1903fbd50 -r 89b1a136edef src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Wed Apr 14 22:07:01 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed Apr 14 22:08:47 2010 +0200
@@ -88,31 +88,39 @@
 
   /* expand_path */
 
+  private val Root = new Regex("(//+[^/]*|/)(.*)")
+  private val Only_Root = new Regex("//+[^/]*|/")
+
   def expand_path(isabelle_path: String): String =
   {
     val result_path = new StringBuilder
-    def init(path: String)
+    def init(path: String): String =
     {
-      if (path.startsWith("/")) {
-        result_path.clear
-        result_path += '/'
+      path match {
+        case Root(root, rest) =>
+          result_path.clear
+          result_path ++= root
+          rest
+        case _ => path
       }
     }
     def append(path: String)
     {
-      init(path)
-      for (p <- path.split("/") if p != "" && p != ".") {
+      val rest = init(path)
+      for (p <- rest.split("/") if p != "" && p != ".") {
         if (p == "..") {
           val result = result_path.toString
-          val i = result.lastIndexOf("/")
-          if (result == "")
-            result_path ++= ".."
-          else if (result.substring(i + 1) == "..")
-            result_path ++= "/.."
-          else if (i < 1)
-            result_path.length = i + 1
-          else
-            result_path.length = i
+          if (!Only_Root.pattern.matcher(result).matches) {
+            val i = result.lastIndexOf("/")
+            if (result == "")
+              result_path ++= ".."
+            else if (result.substring(i + 1) == "..")
+              result_path ++= "/.."
+            else if (i < 0)
+              result_path.length = 0
+            else
+              result_path.length = i
+          }
         }
         else {
           val len = result_path.length
@@ -122,8 +130,8 @@
         }
       }
     }
-    init(isabelle_path)
-    for (p <- isabelle_path.split("/")) {
+    val rest = init(isabelle_path)
+    for (p <- rest.split("/")) {
       if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
       else if (p == "~") append(getenv_strict("HOME"))
       else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
diff -r 89d1903fbd50 -r 89b1a136edef src/Pure/System/standard_system.scala
--- a/src/Pure/System/standard_system.scala	Wed Apr 14 22:07:01 2010 +0200
+++ b/src/Pure/System/standard_system.scala	Wed Apr 14 22:08:47 2010 +0200
@@ -162,6 +162,7 @@
   /* jvm_path */
 
   private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
+  private val Named_Root = new Regex("//+([^/]*)(.*)")
 
   def jvm_path(posix_path: String): String =
     if (Platform.is_windows) {
@@ -171,6 +172,11 @@
           case Cygdrive(drive, rest) =>
             result_path ++= (drive + ":" + File.separator)
             rest
+          case Named_Root(root, rest) =>
+            result_path ++= File.separator
+            result_path ++= File.separator
+            result_path ++= root
+            rest
           case path if path.startsWith("/") =>
             result_path ++= platform_root
             path