src/Pure/General/path.ML
changeset 21858 05f57309170c
parent 19482 9f11af8f7ef9
child 23672 3fd7770f6795
     1.1 --- a/src/Pure/General/path.ML	Thu Dec 14 22:19:39 2006 +0100
     1.2 +++ b/src/Pure/General/path.ML	Fri Dec 15 00:08:06 2006 +0100
     1.3 @@ -21,8 +21,8 @@
     1.4    val append: T -> T -> T
     1.5    val appends: T list -> T
     1.6    val make: string list -> T
     1.7 -  val pack: T -> string
     1.8 -  val unpack: string -> T
     1.9 +  val implode: T -> string
    1.10 +  val explode: string -> T
    1.11    val dir: T -> T
    1.12    val base: T -> T
    1.13    val ext: string -> T -> T
    1.14 @@ -95,35 +95,35 @@
    1.15  fun norm path = rev_app [] path;
    1.16  
    1.17  
    1.18 -(* pack *)
    1.19 +(* implode *)
    1.20  
    1.21 -fun pack_elem Root = ""
    1.22 -  | pack_elem Parent = ".."
    1.23 -  | pack_elem (Basic s) = s
    1.24 -  | pack_elem (Variable s) = "$" ^ s;
    1.25 +fun implode_elem Root = ""
    1.26 +  | implode_elem Parent = ".."
    1.27 +  | implode_elem (Basic s) = s
    1.28 +  | implode_elem (Variable s) = "$" ^ s;
    1.29  
    1.30 -fun pack (Path []) = "."
    1.31 -  | pack (Path (Root :: xs)) = "/" ^ space_implode "/" (map pack_elem xs)
    1.32 -  | pack (Path xs) = space_implode "/" (map pack_elem xs);
    1.33 +fun implode_path (Path []) = "."
    1.34 +  | implode_path (Path (Root :: xs)) = "/" ^ space_implode "/" (map implode_elem xs)
    1.35 +  | implode_path (Path xs) = space_implode "/" (map implode_elem xs);
    1.36  
    1.37  
    1.38 -(* unpack *)
    1.39 +(* explode *)
    1.40  
    1.41 -fun unpack_elem "" = Root
    1.42 -  | unpack_elem ".." = Parent
    1.43 -  | unpack_elem "~" = Variable "HOME"
    1.44 -  | unpack_elem "~~" = Variable "ISABELLE_HOME"
    1.45 -  | unpack_elem s =
    1.46 +fun explode_elem "" = Root
    1.47 +  | explode_elem ".." = Parent
    1.48 +  | explode_elem "~" = Variable "HOME"
    1.49 +  | explode_elem "~~" = Variable "ISABELLE_HOME"
    1.50 +  | explode_elem s =
    1.51        (case explode s of
    1.52          "$" :: cs => variable_elem cs
    1.53        | cs => basic_elem cs);
    1.54  
    1.55 -val unpack_elems = map unpack_elem o filter_out (fn c => c = "" orelse c = ".");
    1.56 +val explode_elems = map explode_elem o filter_out (fn c => c = "" orelse c = ".");
    1.57  
    1.58 -fun unpack str = Path (norm
    1.59 +fun explode_path str = Path (norm
    1.60    (case space_explode "/" str of
    1.61 -    "" :: ss => Root :: unpack_elems ss
    1.62 -  | ss => unpack_elems ss));
    1.63 +    "" :: ss => Root :: explode_elems ss
    1.64 +  | ss => explode_elems ss));
    1.65  
    1.66  
    1.67  (* base element *)
    1.68 @@ -131,7 +131,7 @@
    1.69  fun split_path f (path as Path xs) =
    1.70    (case try split_last xs of
    1.71      SOME (prfx, Basic s) => f (prfx, s)
    1.72 -  | _ => error ("Cannot split path into dir/base: " ^ quote (pack path)));
    1.73 +  | _ => error ("Cannot split path into dir/base: " ^ quote (implode_path path)));
    1.74  
    1.75  val dir = split_path (fn (prfx, _) => Path prfx);
    1.76  val base = split_path (fn (_, s) => Path [Basic s]);
    1.77 @@ -150,10 +150,15 @@
    1.78  fun eval (Variable s) =
    1.79      (case getenv s of
    1.80        "" => error ("Undefined Isabelle environment variable: " ^ quote s)
    1.81 -    | path => rep (unpack path))
    1.82 +    | path => rep (explode_path path))
    1.83    | eval x = [x];
    1.84  
    1.85  val expand = rep #> maps eval #> norm #> Path;
    1.86 -val position = expand #> pack #> quote #> Position.line_name 1;
    1.87 +val position = expand #> implode_path #> quote #> Position.line_name 1;
    1.88 +
    1.89 +
    1.90 +(*final declarations of this structure!*)
    1.91 +val implode = implode_path;
    1.92 +val explode = explode_path;
    1.93  
    1.94  end;