# HG changeset patch
# User wenzelm
# Date 897472288 -7200
# Node ID 37c253fd3dc62f54cb0d0838a3e65f97622086cc
# Parent  9101b70b696d2255dfbde3dc72fc257d496fd560
moved Thy/path.ML to General/path.ML;

diff -r 9101b70b696d -r 37c253fd3dc6 src/Pure/General/path.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/path.ML	Wed Jun 10 11:51:28 1998 +0200
@@ -0,0 +1,104 @@
+(*  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;
diff -r 9101b70b696d -r 37c253fd3dc6 src/Pure/Thy/path.ML
--- 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;