# HG changeset patch
# User wenzelm
# Date 940889045 -7200
# Node ID 2010ae0393ca02f0c7276186d02b299eea5dba1a
# Parent  06a11f8cf573f379eefcb70d401bd69d42ba129c
added drop_ext;
tuned;

diff -r 06a11f8cf573 -r 2010ae0393ca src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Mon Oct 25 20:38:03 1999 +0200
+++ b/src/Pure/General/path.ML	Tue Oct 26 00:04:05 1999 +0200
@@ -25,6 +25,7 @@
   val unpack: string -> T
   val base: T -> T
   val ext: string -> T -> T
+  val drop_ext: T -> T
   val dir: T -> T
   val expand: T -> T
   val position: T -> Position.T
@@ -127,23 +128,22 @@
 
 (* base element *)
 
-fun err_no_base path =
-  error ("No base path element in " ^ quote (pack path));
+fun split_path f (path as Path xs) =
+  (case try split_last xs of
+    Some (prfx, Basic s) => f (prfx, s)
+  | _ => error ("Cannot split path into dir/base: " ^ quote (pack path)));
 
-fun base (path as Path xs) =
-  (case try split_last xs of
-    Some (_, x as Basic _) => Path [x]
-  | _ => err_no_base path);
+val base = split_path (fn (_, s) => Path [Basic s]);
 
-fun ext e (path as Path xs) =
-  (case try split_last xs of
-    Some (prfx, Basic s) => if e = "" then path else Path (prfx @ [Basic (s ^ "." ^ e)])
-  | _ => err_no_base path);
+fun ext "" path = path
+  | ext e path = split_path (fn (prfx, s) => append (Path prfx) (basic (s ^ "." ^ e))) path;
 
-fun dir (path as Path xs) =
-  (case try split_last xs of
-    Some (prfx, _) => Path prfx
-  | _ => error ("Cannot split path " ^ quote (pack path)));
+val drop_ext = split_path (fn (prfx, s) => append (Path prfx)
+  (case take_suffix (not_equal ".") (explode s) of
+    ([], _) => Path [Basic s]
+  | (cs, _) => Path [Basic (implode (take (length cs - 1, cs)))]));
+
+val dir = split_path (fn (prfx, _) => Path prfx);
 
 
 (* evaluate variables *)