added split_ext; removed drop_ext;
authorwenzelm
Wed Jun 09 18:56:55 2004 +0200 (2004-06-09)
changeset 1491288b9d9165452
parent 14911 396a1f4b9c14
child 14913 e993eabc7197
added split_ext; removed drop_ext;
src/Pure/General/path.ML
     1.1 --- a/src/Pure/General/path.ML	Wed Jun 09 18:56:47 2004 +0200
     1.2 +++ b/src/Pure/General/path.ML	Wed Jun 09 18:56:55 2004 +0200
     1.3 @@ -24,10 +24,10 @@
     1.4    val make: string list -> T
     1.5    val pack: T -> string
     1.6    val unpack: string -> T
     1.7 +  val dir: T -> T
     1.8    val base: T -> T
     1.9    val ext: string -> T -> T
    1.10 -  val drop_ext: T -> T
    1.11 -  val dir: T -> T
    1.12 +  val split_ext: T -> T * string
    1.13    val expand: T -> T
    1.14    val position: T -> Position.T
    1.15  end;
    1.16 @@ -134,17 +134,16 @@
    1.17      Some (prfx, Basic s) => f (prfx, s)
    1.18    | _ => error ("Cannot split path into dir/base: " ^ quote (pack path)));
    1.19  
    1.20 +val dir = split_path (fn (prfx, _) => Path prfx);
    1.21  val base = split_path (fn (_, s) => Path [Basic s]);
    1.22  
    1.23  fun ext "" path = path
    1.24    | ext e path = split_path (fn (prfx, s) => append (Path prfx) (basic (s ^ "." ^ e))) path;
    1.25  
    1.26 -val drop_ext = split_path (fn (prfx, s) => append (Path prfx)
    1.27 +val split_ext = split_path (fn (prfx, s) => apfst (append (Path prfx))
    1.28    (case take_suffix (not_equal ".") (explode s) of
    1.29 -    ([], _) => Path [Basic s]
    1.30 -  | (cs, _) => Path [Basic (implode (take (length cs - 1, cs)))]));
    1.31 -
    1.32 -val dir = split_path (fn (prfx, _) => Path prfx);
    1.33 +    ([], _) => (Path [Basic s], "")
    1.34 +  | (cs, e) => (Path [Basic (implode (take (length cs - 1, cs)))], implode e)));
    1.35  
    1.36  
    1.37  (* evaluate variables *)