# HG changeset patch
# User wenzelm
# Date 920977791 -3600
# Node ID 80173cb8691c80a7962c2a1cf27f4eb7dae636c1
# Parent  4a423e8a0b5404c5c5b26f66dffb4cf4eac6af4e
added make, dir;

diff -r 4a423e8a0b54 -r 80173cb8691c src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Tue Mar 09 12:09:22 1999 +0100
+++ b/src/Pure/General/path.ML	Tue Mar 09 12:09:51 1999 +0100
@@ -19,10 +19,12 @@
   val is_basic: T -> bool
   val append: T -> T -> T
   val appends: T list -> T
+  val make: string list -> T
   val pack: T -> string
   val unpack: string -> T
   val base: T -> T
   val ext: string -> T -> T
+  val dir: T -> T
   val expand: T -> T
 end;
 
@@ -36,7 +38,8 @@
 
 fun err_elem msg chs = error (msg ^ " path element specification: " ^ quote (implode chs));
 
-fun check_elem (chs as ["~"]) = err_elem "Illegal" chs
+fun check_elem (chs as []) = err_elem "Illegal" chs
+  | check_elem (chs as ["~"]) = err_elem "Illegal" chs
   | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs
   | check_elem chs =
       (case ["/", "\\", "$", ":"] inter_string chs of
@@ -82,6 +85,7 @@
 
 fun append (Path xs) (Path ys) = Path (rev_app (rev xs) ys);
 fun appends paths = foldl (uncurry append) (current, paths);
+val make = appends o map basic;
 fun norm path = rev_app [] path;
 
 
@@ -131,6 +135,11 @@
     Some (prfx, Basic s) => if e = "" then path else Path (prfx @ [Basic (s ^ "." ^ e)])
   | _ => err_no_base path);
 
+fun dir (path as Path xs) =
+  (case try split_last xs of
+    Some (prfx, _) => Path prfx
+  | _ => error ("Cannot split path " ^ quote (pack path)));
+
 
 (* evaluate variables *)