changed split_filename, remove_ext;
authorwenzelm
Tue Nov 30 11:07:57 1993 +0100 (1993-11-30)
changeset 1723224c46737ef
parent 171 ab0f93a291b5
child 173 85071e6ad295
changed split_filename, remove_ext;
added base_name;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Tue Nov 30 11:04:07 1993 +0100
     1.2 +++ b/src/Pure/library.ML	Tue Nov 30 11:07:57 1993 +0100
     1.3 @@ -624,9 +624,10 @@
     1.4  
     1.5  (*Convert Unix filename of the form path/file to "path/" and "file" ;
     1.6    if filename contains no slash, then it returns "" and "file" *)
     1.7 -fun split_filename name =
     1.8 -  let val (file,path) = take_prefix (apr(op<>,"/")) (rev (explode name))
     1.9 -  in  (implode(rev path), implode(rev file)) end;
    1.10 +val split_filename =
    1.11 +  (pairself implode) o take_suffix (not_equal "/") o explode;
    1.12 +
    1.13 +val base_name = #2 o split_filename;
    1.14  
    1.15  (*Merge splitted filename (path and file);
    1.16    if path does not end with one a slash is appended *)
    1.17 @@ -636,7 +637,4 @@
    1.18        else path ^ "/" ^ name;
    1.19  
    1.20  (*Remove the extension of a filename, i.e. the part after the last '.' *)
    1.21 -fun remove_ext name =
    1.22 -  let val (file,_) = take_prefix (apr(op<>,".")) (rev (explode name))
    1.23 -  in implode (rev file) end;
    1.24 -
    1.25 +val remove_ext = implode o #1 o take_suffix (not_equal ".") o explode;