# HG changeset patch
# User wenzelm
# Date 1271276008 -7200
# Node ID 42d690c1cd315698d179a15c5785e2f02b5a30af
# Parent  e8db171b86432960fbf1f08b9debcea947039ea6# Parent  89b1a136edef1ddb940fc9fa45bd9db537c8743a
merged

diff -r e8db171b8643 -r 42d690c1cd31 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Wed Apr 14 21:22:48 2010 +0200
+++ b/src/Pure/General/path.ML	Wed Apr 14 22:13:28 2010 +0200
@@ -1,7 +1,8 @@
 (*  Title:      Pure/General/path.ML
     Author:     Markus Wenzel, TU Muenchen
 
-Abstract algebra of file paths (external encoding in Unix style).
+Abstract algebra of file paths: basic POSIX notation, extended by
+named roots (e.g. //foo) and variables (e.g. $BAR).
 *)
 
 signature PATH =
@@ -10,6 +11,7 @@
   val is_current: T -> bool
   val current: T
   val root: T
+  val named_root: string -> T
   val parent: T
   val basic: string -> T
   val variable: string -> T
@@ -31,10 +33,15 @@
 structure Path: PATH =
 struct
 
-
 (* path elements *)
 
-datatype elem = Root | Parent | Basic of string | Variable of string;
+datatype elem =
+  Root of string |
+  Basic of string |
+  Variable of string |
+  Parent;
+
+local
 
 fun err_elem msg chs = error (msg ^ " path element specification: " ^ quote (implode chs));
 
@@ -46,16 +53,18 @@
         [] => chs
       | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs);
 
+in
+
+val root_elem = Root o implode o check_elem;
 val basic_elem = Basic o implode o check_elem;
 val variable_elem = Variable o implode o check_elem;
 
-fun is_var (Variable _) = true
-  | is_var _ = false;
+end;
 
 
 (* type path *)
 
-datatype T = Path of elem list;
+datatype T = Path of elem list;    (*reversed elements*)
 
 fun rep (Path xs) = xs;
 
@@ -63,13 +72,16 @@
   | is_current _ = false;
 
 val current = Path [];
-val root = Path [Root];
-val parent = Path [Parent];
+val root = Path [Root ""];
+fun named_root s = Path [root_elem (explode s)];
 fun basic s = Path [basic_elem (explode s)];
 fun variable s = Path [variable_elem (explode s)];
+val parent = Path [Parent];
 
-fun is_absolute (Path (Root :: _)) = true
-  | is_absolute _ = false;
+fun is_absolute (Path xs) =
+  (case try List.last xs of
+    SOME (Root _) => true
+  | _ => false);
 
 fun is_basic (Path [Basic _]) = true
   | is_basic _ = false;
@@ -77,37 +89,42 @@
 
 (* append and norm *)
 
-(*append non-normal path (2n arg) to reversed normal one, result is normal*)
-fun rev_app xs [] = rev xs
-  | rev_app _ (Root :: ys) = rev_app [Root] ys
-  | rev_app (x :: xs) (Parent :: ys) =
-      if x = Parent orelse is_var x then rev_app (Parent :: x :: xs) ys
-      else if x = Root then rev_app (x :: xs) ys
-      else rev_app xs ys
-  | rev_app xs (y :: ys) = rev_app (y :: xs) ys;
+fun apply (y as Root _) _ = [y]
+  | apply Parent (xs as (Root _ :: _)) = xs
+  | apply Parent (Basic _ :: rest) = rest
+  | apply y xs = y :: xs;
 
-fun append (Path xs) (Path ys) = Path (rev_app (rev xs) ys);
+fun append (Path xs) (Path ys) = Path (fold_rev apply ys xs);
 fun appends paths = Library.foldl (uncurry append) (current, paths);
 val make = appends o map basic;
-fun norm path = rev_app [] path;
+
+fun norm elems = fold_rev apply elems [];
 
 
 (* implode *)
 
-fun implode_elem Root = ""
-  | implode_elem Parent = ".."
+local
+
+fun implode_elem (Root "") = ""
+  | implode_elem (Root s) = "//" ^ s
   | implode_elem (Basic s) = s
-  | implode_elem (Variable s) = "$" ^ s;
+  | implode_elem (Variable s) = "$" ^ s
+  | implode_elem Parent = "..";
+
+in
 
 fun implode_path (Path []) = "."
-  | implode_path (Path (Root :: xs)) = "/" ^ space_implode "/" (map implode_elem xs)
-  | implode_path (Path xs) = space_implode "/" (map implode_elem xs);
+  | implode_path (Path [Root ""]) = "/"
+  | implode_path (Path xs) = space_implode "/" (rev (map implode_elem xs));
+
+end;
 
 
 (* explode *)
 
-fun explode_elem "" = Root
-  | explode_elem ".." = Parent
+local
+
+fun explode_elem ".." = Parent
   | explode_elem "~" = Variable "HOME"
   | explode_elem "~~" = Variable "ISABELLE_HOME"
   | explode_elem s =
@@ -115,28 +132,35 @@
         "$" :: cs => variable_elem cs
       | cs => basic_elem cs);
 
-val explode_elems = map explode_elem o filter_out (fn c => c = "" orelse c = ".");
+val explode_elems =
+  rev o map explode_elem o filter_out (fn c => c = "" orelse c = ".");
+
+in
 
-fun explode_path str = Path (norm
-  (case space_explode "/" str of
-    "" :: ss => Root :: explode_elems ss
-  | ss => explode_elems ss));
+fun explode_path str =
+  let val (roots, raw_elems) =
+    (case take_prefix (equal "") (space_explode "/" str) |>> length of
+      (0, es) => ([], es)
+    | (1, es) => ([Root ""], es)
+    | (_, []) => ([Root ""], [])
+    | (_, e :: es) => ([root_elem (explode e)], es))
+  in Path (norm (explode_elems raw_elems @ roots)) end;
+
+end;
 
 
 (* base element *)
 
-fun split_path f (path as Path xs) =
-  (case try split_last xs of
-    SOME (prfx, Basic s) => f (prfx, s)
-  | _ => error ("Cannot split path into dir/base: " ^ quote (implode_path path)));
+fun split_path f (Path (Basic s :: xs)) = f (Path xs, s)
+  | split_path _ path = error ("Cannot split path into dir/base: " ^ quote (implode_path path));
 
-val dir = split_path (fn (prfx, _) => Path prfx);
+val dir = split_path #1;
 val base = split_path (fn (_, s) => Path [Basic s]);
 
-fun ext "" path = path
-  | ext e path = split_path (fn (prfx, s) => append (Path prfx) (basic (s ^ "." ^ e))) path;
+fun ext "" = I
+  | ext e = split_path (fn (prfx, s) => append prfx (basic (s ^ "." ^ e)));
 
-val split_ext = split_path (fn (prfx, s) => apfst (append (Path prfx))
+val split_ext = split_path (fn (prfx, s) => apfst (append prfx)
   (case take_suffix (fn c => c <> ".") (explode s) of
     ([], _) => (Path [Basic s], "")
   | (cs, e) => (Path [Basic (implode (take (length cs - 1) cs))], implode e)));
@@ -144,14 +168,20 @@
 
 (* expand variables *)
 
+local
+
 fun eval (Variable s) =
-    (case getenv s of
-      "" => error ("Undefined Isabelle environment variable: " ^ quote s)
-    | path => rep (explode_path path))
+      (case getenv s of
+        "" => error ("Undefined Isabelle environment variable: " ^ quote s)
+      | path => rep (explode_path path))
   | eval x = [x];
 
+in
+
 val expand = rep #> maps eval #> norm #> Path;
 
+end;
+
 
 (* source position *)
 
@@ -163,3 +193,4 @@
 val explode = explode_path;
 
 end;
+
diff -r e8db171b8643 -r 42d690c1cd31 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Wed Apr 14 21:22:48 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed Apr 14 22:13:28 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 e8db171b8643 -r 42d690c1cd31 src/Pure/System/standard_system.scala
--- a/src/Pure/System/standard_system.scala	Wed Apr 14 21:22:48 2010 +0200
+++ b/src/Pure/System/standard_system.scala	Wed Apr 14 22:13:28 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