# HG changeset patch
# User wenzelm
# Date 1129327691 -7200
# Node ID ecd890746fcfded677bb7cdde80d999aaf93b463
# Parent  28d3483afbbc09880a464cced3dcfeaaaff60004
use perl for test/stat;

diff -r 28d3483afbbc -r ecd890746fcf src/Pure/ML-Systems/poplogml.ML
--- a/src/Pure/ML-Systems/poplogml.ML	Sat Oct 15 00:08:10 2005 +0200
+++ b/src/Pure/ML-Systems/poplogml.ML	Sat Oct 15 00:08:11 2005 +0200
@@ -304,8 +304,7 @@
 
 fun squote s = "'" ^ s ^ "'";
 fun remove name = (execute_rc ("/bin/rm -- " ^ squote name); ());
-fun is_dir name = execute_rc ("test -d " ^ squote name) = 0;
-fun is_present name = execute_rc ("test -e " ^ squote name) = 0;
+fun is_dir name = execute_rc ("perl -e \"exit (-d " ^ squote name ^ " ? 0 : 1)\"") = 0;
 
 fun execute_result cmdline =
   let
@@ -317,9 +316,6 @@
     val _ = remove tmp;
   in (rc, result) end;
 
-fun int_of_string s =
-  Int.fromString (if String.isSuffix "\n" s then String.substring (s, 0, size s - 1) else s);
-
 in
 
 fun exit rc = shell ("exit " ^ Int.toString rc);
@@ -347,12 +343,13 @@
     val compare = Int.compare;
 
     fun modTime name =
-      if is_present name then int_of_string (execute ("stat -c '%Y' " ^ squote name))
-      else raise TextIO.Io "OS.FileSys.modTime";
-
+      (case execute ("perl -e '@_ = stat(q:" ^ name ^ ":); print $_[9]'") of
+        "" => raise TextIO.Io "OS.FileSys.modTime"
+      | s => Int.fromString s);
     fun fileId name =
-      if is_present name then int_of_string (execute ("stat -c '%i' " ^ squote name))
-      else raise TextIO.Io "OS.FileSys.fileId";
+      (case execute ("perl -e '@_ = stat(q:" ^ name ^ ":); print $_[1]'") of
+        "" => raise TextIO.Io "OS.FileSys.fileId"
+      | s => Int.fromString s);
   end;
 end;