# HG changeset patch
# User clasohm
# Date 752851485 -3600
# Node ID e95b98536b3df78e83b550607e2ad3f4b5cc92b0
# Parent  df0cd0fecf866b1bc612d4141edaf5147771fdf4
fixed a bug in POLY.ML: delete_file didn't close streams;
added function pwd to get current working directory

diff -r df0cd0fecf86 -r e95b98536b3d src/Pure/NJ.ML
--- a/src/Pure/NJ.ML	Tue Nov 09 13:32:45 1993 +0100
+++ b/src/Pure/NJ.ML	Tue Nov 09 14:24:45 1993 +0100
@@ -94,3 +94,5 @@
   let val _ = System.system ("rm " ^ name)
   in () end;
 
+(*Get pathname of current working directory *)
+fun pwd () = System.Directory.getWD ();
diff -r df0cd0fecf86 -r e95b98536b3d src/Pure/POLY.ML
--- a/src/Pure/POLY.ML	Tue Nov 09 13:32:45 1993 +0100
+++ b/src/Pure/POLY.ML	Tue Nov 09 14:24:45 1993 +0100
@@ -38,19 +38,25 @@
 
 (*** File handling ***)
 
+local
+
+(*These are functions from library.ML *)
+fun take_suffix _ [] = ([], [])
+  | take_suffix pred (x :: xs) =
+      (case take_suffix pred xs of
+         ([], sffx) => if pred x then ([], x :: sffx)
+                                 else ([x], sffx)
+       | (prfx, sffx) => (x :: prfx, sffx));
+
+fun apr (f,y) x = f(x,y);
+
+in
+
 (*Get a string containing the time of last modification, attributes, owner
   and size of file (but not the path) *)
 fun file_info "" = ""
   | file_info name =
       let
-          (*These are functions from library.ML *)
-          fun take_suffix _ [] = ([], [])
-            | take_suffix pred (x :: xs) =
-                (case take_suffix pred xs of
-                  ([], sffx) => if pred x then ([], x :: sffx) else ([x], sffx)
-                | (prfx, sffx) => (x :: prfx, sffx));
-          fun apr (f,y) x = f(x,y);
-
           val (is, os) = ExtendedIO.execute ("ls -l " ^ name)
           val (result, _) = take_suffix (apr(op<>," ")) 
                               (explode (ExtendedIO.input_line is))
@@ -62,5 +68,20 @@
 
 (*Delete a file *)
 fun delete_file name =
-  let val (_,_) = ExtendedIO.execute ("rm " ^ name)
-  in () end;
+  let val (is, os) = ExtendedIO.execute ("rm " ^ name)
+  in close_in is;
+     close_out os
+  end;
+
+(*Get pathname of current working directory *)
+fun pwd () =
+  let val (is, os) = ExtendedIO.execute ("pwd")
+      val (path, _) = take_suffix (apr(op=,"\n"))
+                       (explode (ExtendedIO.input_line is)) (*remove newline *)
+  in close_in is;
+     close_out os;
+     implode path
+  end;
+
+end;
+