diff -r 4a07dfe3583f -r ca3ff2fee318 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Wed Feb 03 16:32:32 1999 +0100
+++ b/src/Pure/General/path.ML	Wed Feb 03 16:36:38 1999 +0100
@@ -2,103 +2,141 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Abstract algebra of file paths.  External representation Unix-style.
+Abstract algebra of file paths (external encoding Unix-style).
 *)
 
 signature PATH =
 sig
-  type T
+  datatype elem = Root | Parent | Basic of string | Variable of string
+  eqtype T
+  val rep: T -> elem list
+  val current: T
+  val root: T
+  val parent: T
+  val basic: string -> T
+  val variable: string -> T
+  val is_absolute: T -> bool
+  val is_basic: T -> bool
+  val append: T -> T -> T
   val pack: T -> string
   val unpack: string -> T
-  val current: T
-  val parent: T
-  val root: T
-  val variable: string -> T
-  val absolute: T -> bool
-  val base: T -> string
-  val append: T -> T -> T
-  val evaluate: (string -> T) -> T -> T
-  val expand: (string -> string) -> string -> string
-  val base_name: string -> string
-  val is_base: string -> bool
+  val base: T -> T
+  val ext: string -> T -> T
+(* FIXME  val evaluate: (string -> T) -> T -> T	*)
+  val expand: T -> T
 end;
 
-structure Path: PATH =
+structure Path(* FIXME : PATH *) =
 struct
 
+
+(* path elements *)
+
+datatype elem = Root | Parent | Basic of string | Variable of string;
+
+fun no_meta_chars chs =
+  (case ["/", "\\", "$", "~"] inter_string chs of
+    [] => chs
+  | bads => error ("Illegal character(s) " ^ commas_quote bads ^
+      " in path element specification: " ^ quote (implode chs)));
+
+val basic_elem = Basic o implode o no_meta_chars;
+val variable_elem = Variable o implode o no_meta_chars;
+
+fun is_var (Variable _) = true
+  | is_var _ = false;
+
+
 (* type path *)
 
-datatype T = Path of string list;
+datatype T = Path of elem list;
+
+fun rep (Path xs) = xs;
 
 val current = Path [];
-val parent = Path [".."];
-val root = Path ["/"];
-
-fun absolute (Path ("/" :: _)) = true
-  | absolute _ = false;
+val root = Path [Root];
+val parent = Path [Parent];
+fun basic s = Path [basic_elem (explode s)];
+fun variable s = Path [variable_elem (explode s)];
 
-fun base (Path []) = ""
-  | base (Path ["/"]) = ""
-  | base (Path xs) = snd (split_last xs);
+fun is_absolute (Path (Root :: _)) = true
+  | is_absolute _ = false;
 
-fun variable name = Path ["$" ^ name];
-fun is_variable elem = ord elem = ord "$";
+fun is_basic (Path [Basic _]) = true
+  | is_basic _ = false;
 
 
 (* append and norm *)
 
 (*append non-normal path (2n arg) to reversed normal one, result is normal*)
 fun rev_app xs [] = rev xs
-  | rev_app _ ("/" :: ys) = rev_app ["/"] ys
-  | rev_app xs ("." :: ys) = rev_app xs ys
-  | rev_app (x :: xs) (".." :: ys) =
-      if x = ".." orelse is_variable x then rev_app (".." :: x :: xs) ys
-      else if x = "/" then rev_app (x :: xs) ys
+  | 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 append (Path xs) (Path ys) = Path (rev_app (rev xs) ys);
 fun norm path = rev_app [] path;
 
-fun append (Path xs) (Path ys) = Path (rev_app (rev xs) ys);
+
+(* pack *)
 
-
-(* pack and unpack *)
+fun pack_elem Root = ""
+  | pack_elem Parent = ".."
+  | pack_elem (Basic s) = s
+  | pack_elem (Variable s) = "$" ^ s;
 
 fun pack (Path []) = "."
-  | pack (Path ("/" :: xs)) = "/" ^ space_implode "/" xs
-  | pack (Path xs) = space_implode "/" xs;
-
-fun unpack str =
-  (case space_explode "/" str of
-    [""] => []
-  | "" :: xs => "/" :: filter (not_equal "") xs
-  | xs => filter (not_equal "") xs)
-    |> map (fn "~" => "$HOME" | x => x)
-    |> norm
-    |> Path;
+  | pack (Path (Root :: xs)) = "/" ^ space_implode "/" (map pack_elem xs)
+  | pack (Path xs) = space_implode "/" (map pack_elem xs);
 
 
-(* eval variables *)
+(* unpack *)
+
+fun unpack_elem "" = Root
+  | unpack_elem ".." = Parent
+  | unpack_elem "~" = Variable "HOME"
+  | unpack_elem "~~" = Variable "ISABELLE_HOME"
+  | unpack_elem s =
+      (case explode s of
+        "$" :: cs => variable_elem cs
+      | cs => basic_elem cs);
+
+val unpack_elems = map unpack_elem o filter_out (equal "" orf equal ".");
+
+fun unpack str = Path (norm
+  (case space_explode "/" str of
+    "" :: ss => Root :: unpack_elems ss
+  | ss => unpack_elems ss));
+
 
-fun eval env x =
-  if is_variable x then
-    let val Path ys = env (implode (tl (explode x)))
-    in ys end
-  else [x];
+(* base element *)
+
+fun err_no_base path =
+  error ("No base path element in " ^ quote (pack path));
+
+fun base (path as Path xs) =
+  (case try split_last xs of
+    Some (_, x as Basic _) => Path [x]
+  | _ => err_no_base path);
+
+fun ext e (path as Path xs) =
+  (case try split_last xs of
+    Some (prfx, Basic s) => if e = "" then path else Path (prfx @ [Basic (s ^ "." ^ e)])
+  | _ => err_no_base path);
+
+
+(* evaluate variables *)
+
+fun eval env (Variable s) = rep (env s)
+  | eval _ x = [x];
 
 fun evaluate env (Path xs) =
   Path (norm (flat (map (eval env) xs)));
 
-
-(* operations on packed paths *)
-
-fun expand env str =
-  pack (evaluate (unpack o env) (unpack str));
-
-val base_name = base o unpack;
-
-fun is_base str =
-  not (exists (equal "/" orf equal "$") (explode str));
+val expand = evaluate (unpack o getenv);
 
 
 end;