--- a/src/Pure/Thy/path.ML Wed Jun 10 11:50:52 1998 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,104 +0,0 @@
-(* Title: Pure/Thy/path.ML
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-
-Abstract algebra of file paths. External representation Unix-style.
-*)
-
-signature PATH =
-sig
- type 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
-end;
-
-structure Path: PATH =
-struct
-
-(* type path *)
-
-datatype T = Path of string list;
-
-val current = Path [];
-val parent = Path [".."];
-val root = Path ["/"];
-
-fun absolute (Path ("/" :: _)) = true
- | absolute _ = false;
-
-fun base (Path []) = ""
- | base (Path ["/"]) = ""
- | base (Path xs) = snd (split_last xs);
-
-fun variable name = Path ["$" ^ name];
-fun is_variable elem = ord elem = ord "$";
-
-
-(* 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
- else 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 ("/" :: 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;
-
-
-(* eval variables *)
-
-fun eval env x =
- if is_variable x then
- let val Path ys = env (implode (tl (explode x)))
- in ys end
- else [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));
-
-
-end;