src/Pure/library.ML
changeset 24 f3d4ff75d9f2
parent 0 a5a9c433f639
child 41 97aae241094b
equal deleted inserted replaced
23:1cd377c2f7c6 24:f3d4ff75d9f2
     1 (*  Title: 	library
     1 (*  Title:      library
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     4     Copyright   1992  University of Cambridge
     5 
     5 
     6 Basic library: booleans, lists, pairs, input/output, etc.
     6 Basic library: booleans, lists, pairs, input/output, etc.
   581   let fun scan1 [] = []
   581   let fun scan1 [] = []
   582 	| scan1 cs =
   582 	| scan1 cs =
   583 	    let val (lets, rest) = take_prefix is_let cs
   583 	    let val (lets, rest) = take_prefix is_let cs
   584 	    in  implode lets :: scanwords is_let rest  end;
   584 	    in  implode lets :: scanwords is_let rest  end;
   585   in  scan1 (#2 (take_prefix (not o is_let) cs))  end;
   585   in  scan1 (#2 (take_prefix (not o is_let) cs))  end;
       
   586 
       
   587 
       
   588 (*** Operations on filenames ***)
       
   589 
       
   590 (*Convert Unix filename of the form path/file to "path/" and "file" ;
       
   591   if filename contains no slash, then it returns "" and "file" *)
       
   592 fun split_filename name =
       
   593   let val (file,path) = take_prefix (apr(op<>,"/")) (rev (explode name))
       
   594   in  (implode(rev path), implode(rev file)) end;
       
   595 
       
   596 (*Merge splitted filename (path and file);
       
   597   if path does not end with one a slash is appended *)
       
   598 fun tack_on "" name = name
       
   599   | tack_on path name =
       
   600       if (hd (rev (explode path))) = "/" then path ^ name
       
   601                                          else path ^ "/" ^ name;
       
   602 
       
   603 (*Remove the extension of a filename, i.e. the part after the last '.' *)
       
   604 fun remove_ext name =
       
   605   let val (file,_) = take_prefix (apr(op<>,".")) (rev (explode name))
       
   606   in implode (rev file) end;
       
   607