src/Pure/General/path.ML
changeset 6319 80173cb8691c
parent 6270 c905fe5994a2
child 6460 cb8c85435228
     1.1 --- a/src/Pure/General/path.ML	Tue Mar 09 12:09:22 1999 +0100
     1.2 +++ b/src/Pure/General/path.ML	Tue Mar 09 12:09:51 1999 +0100
     1.3 @@ -19,10 +19,12 @@
     1.4    val is_basic: T -> bool
     1.5    val append: T -> T -> T
     1.6    val appends: T list -> T
     1.7 +  val make: string list -> T
     1.8    val pack: T -> string
     1.9    val unpack: string -> T
    1.10    val base: T -> T
    1.11    val ext: string -> T -> T
    1.12 +  val dir: T -> T
    1.13    val expand: T -> T
    1.14  end;
    1.15  
    1.16 @@ -36,7 +38,8 @@
    1.17  
    1.18  fun err_elem msg chs = error (msg ^ " path element specification: " ^ quote (implode chs));
    1.19  
    1.20 -fun check_elem (chs as ["~"]) = err_elem "Illegal" chs
    1.21 +fun check_elem (chs as []) = err_elem "Illegal" chs
    1.22 +  | check_elem (chs as ["~"]) = err_elem "Illegal" chs
    1.23    | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs
    1.24    | check_elem chs =
    1.25        (case ["/", "\\", "$", ":"] inter_string chs of
    1.26 @@ -82,6 +85,7 @@
    1.27  
    1.28  fun append (Path xs) (Path ys) = Path (rev_app (rev xs) ys);
    1.29  fun appends paths = foldl (uncurry append) (current, paths);
    1.30 +val make = appends o map basic;
    1.31  fun norm path = rev_app [] path;
    1.32  
    1.33  
    1.34 @@ -131,6 +135,11 @@
    1.35      Some (prfx, Basic s) => if e = "" then path else Path (prfx @ [Basic (s ^ "." ^ e)])
    1.36    | _ => err_no_base path);
    1.37  
    1.38 +fun dir (path as Path xs) =
    1.39 +  (case try split_last xs of
    1.40 +    Some (prfx, _) => Path prfx
    1.41 +  | _ => error ("Cannot split path " ^ quote (pack path)));
    1.42 +
    1.43  
    1.44  (* evaluate variables *)
    1.45