# HG changeset patch
# User clasohm
# Date 749823301 -3600
# Node ID f3d4ff75d9f266e0afed1cf90c3cf1be76f5edb2
# Parent  1cd377c2f7c64a7b420243a62c4ae366e523b1c7
added functions that operate on filenames: split_filename (originally located
in Pure/read.ML), tack_on, remove_ext

diff -r 1cd377c2f7c6 -r f3d4ff75d9f2 src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Oct 04 15:49:49 1993 +0100
+++ b/src/Pure/library.ML	Tue Oct 05 13:15:01 1993 +0100
@@ -1,4 +1,4 @@
-(*  Title: 	library
+(*  Title:      library
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
@@ -583,3 +583,25 @@
 	    let val (lets, rest) = take_prefix is_let cs
 	    in  implode lets :: scanwords is_let rest  end;
   in  scan1 (#2 (take_prefix (not o is_let) cs))  end;
+
+
+(*** Operations on filenames ***)
+
+(*Convert Unix filename of the form path/file to "path/" and "file" ;
+  if filename contains no slash, then it returns "" and "file" *)
+fun split_filename name =
+  let val (file,path) = take_prefix (apr(op<>,"/")) (rev (explode name))
+  in  (implode(rev path), implode(rev file)) end;
+
+(*Merge splitted filename (path and file);
+  if path does not end with one a slash is appended *)
+fun tack_on "" name = name
+  | tack_on path name =
+      if (hd (rev (explode path))) = "/" then path ^ name
+                                         else path ^ "/" ^ name;
+
+(*Remove the extension of a filename, i.e. the part after the last '.' *)
+fun remove_ext name =
+  let val (file,_) = take_prefix (apr(op<>,".")) (rev (explode name))
+  in implode (rev file) end;
+