# HG changeset patch
# User wenzelm
# Date 878643857 -3600
# Node ID 8d80c1a3b546d3bf42d0c4c602a4fd2104872f2e
# Parent  f7130dcacefae83a2e4fc27e0df323e8b3d79f21
added base;
tuned;

diff -r f7130dcacefa -r 8d80c1a3b546 src/Pure/Thy/path.ML
--- a/src/Pure/Thy/path.ML	Tue Nov 04 12:33:51 1997 +0100
+++ b/src/Pure/Thy/path.ML	Tue Nov 04 12:44:17 1997 +0100
@@ -17,6 +17,7 @@
   val parent: T
   val root: T
   val absolute: T -> bool
+  val base: T -> string
   val append: T -> T -> T
 end;
 
@@ -29,39 +30,43 @@
 
 val current = Path [];
 val parent = Path [".."];
-val root = Path [""];
+val root = Path ["/"];
 
-fun absolute (Path ("" :: _)) = true
+fun absolute (Path ("/" :: _)) = true
   | absolute _ = false;
 
+fun base (Path []) = ""
+  | base (Path xs) = snd (split_last xs);
+
 
 (* 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 _ ("/" :: ys) = rev_app ["/"] ys
   | rev_app xs ("." :: ys) = rev_app xs ys
   | rev_app [] (".." :: ys) = rev_app [".."] ys
   | rev_app (xs as ".." :: _) (".." :: ys) = rev_app (".." :: xs) ys
-  | rev_app (xs as "" :: _) (".." :: ys) = rev_app xs ys
+  | rev_app (xs as "/" :: _) (".." :: ys) = rev_app xs ys
   | rev_app (_ :: xs) (".." :: ys) = rev_app xs ys
   | rev_app xs (y :: ys) = rev_app (y :: xs) ys;
 
 fun norm path = rev_app [] path;
+
 fun append (Path xs) (Path ys) = Path (rev_app (rev xs) ys);
 
 
 (* pack and unpack *)
 
 fun pack (Path []) = "."
-  | pack (path as Path xs) =
-      (if absolute path then "/" else "") ^ space_implode "/" xs;
+  | pack (Path ("/" :: xs)) = "/" ^ space_implode "/" xs
+  | pack (Path xs) = space_implode "/" xs;
 
 fun unpack str =
   Path (norm
     (case space_explode "/" str of
       [""] => []
-    | "" :: xs => "" :: filter (not_equal "") xs
+    | "" :: xs => "/" :: filter (not_equal "") xs
     | xs => filter (not_equal "") xs));