# HG changeset patch
# User clasohm
# Date 750685881 -3600
# Node ID b30802dfbe806cf6651d86b4d610d3c2244f80db
# Parent  87e14d7f20dced6af499619b4dd1f452c930e399
file_info now returns a string that does not contain the path/filename
(so the string doesn't change when the relative path does)

diff -r 87e14d7f20dc -r b30802dfbe80 src/Pure/POLY.ML
--- a/src/Pure/POLY.ML	Fri Oct 15 12:49:33 1993 +0100
+++ b/src/Pure/POLY.ML	Fri Oct 15 12:51:21 1993 +0100
@@ -38,12 +38,24 @@
 
 (*** File information ***)
 
-(*Get time of last modification.*)
+(*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 val (is, os) = ExtendedIO.execute ("ls -l " ^ name)
-            val result = ExtendedIO.input_line is;
-            val dummy = close_in is;
-            val dummy = close_out os;
-        in result end;
+      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))
+                (*Remove the part after the last " " (i.e. the path/filename) *)
+        in close_in is;
+           close_out os;
+           implode result
+        end;