Basis library emulation, especially of I/O operations

--- a/src/Pure/NJ093.ML	Wed Nov 27 10:44:09 1996 +0100
+++ b/src/Pure/NJ093.ML	Wed Nov 27 10:45:58 1996 +0100
@@ -7,14 +7,7 @@
 *)
 
 
-(*** Basis Library emulation ***)
-
-structure Int =
-  struct
-  fun max (x, y) = if x < y then y else x : int;
-  fun min (x, y) = if x < y then x else y : int;
-  end;
-
+use"basis.ML";
 
 (*** Poly/ML emulation ***)
 
@@ -22,9 +15,6 @@
 val exit = System.Unsafe.CInterface.exit;
 fun quit () = exit 0;
 
-(*To change the current directory*)
-val cd = System.Directory.cd;
-
 (*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*)
 fun print_depth n = (System.Control.Print.printDepth := n div 2;
                      System.Control.Print.printLength := n);
@@ -89,12 +79,17 @@
 in
   fun file_info "" = ""
     | file_info name = makestring (mtime (PATH name))  handle _ => "";
-
-  val delete_file = unlink;
 end;
 
-(*Get pathname of current working directory *)
-fun pwd () = System.Directory.getWD ();
+structure OS =
+  struct
+  structure FileSys =
+    struct
+    val OS.FileSys.chDir = System.Directory.cd
+    val remove = System.Unsafe.SysIO.unlink       (*Delete a file *)
+    val getDir = System.Directory.getWD           (*path of working directory*)
+    end
+  end;
 
 
 (*** ML command execution ***)
@@ -119,6 +114,9 @@
      result
   end;
 
+(*redefine to flush its output immediately -- temporary patch suggested
+  by Kim Dam Petersen*)
+val output = fn(s, t) => (output(s, t); flush_out s);
 
 (*For use in Makefiles -- saves space*)
 fun xML filename banner = (exportML filename;  print(banner^"\n"));

--- a/src/Pure/POLY.ML	Wed Nov 27 10:44:09 1996 +0100
+++ b/src/Pure/POLY.ML	Wed Nov 27 10:45:58 1996 +0100
@@ -8,13 +8,7 @@
 
 open PolyML ExtendedIO;
 
-
-structure Int =
-  struct
-  fun max (x, y) = if x < y then y else x : int;
-  fun min (x, y) = if x < y then x else y : int;
-  end;
-
+use"basis.ML";
 
 (*A conditional timing function: applies f to () and, if the flag is true,
   prints its runtime.*)
@@ -77,22 +71,27 @@
 fun file_info "" = ""
   | file_info name = radixstring (System.filedate name)  handle _ => "";
 
-(*Delete a file *)
-fun delete_file name =
-  let val (is, os) = ExtendedIO.execute ("rm " ^ name)
-  in close_in is;
-     close_out os
+
+structure OS =
+  struct
+  structure FileSys =
+    struct
+    val chDir = PolyML.cd
+
+    fun remove name =    (*Delete a file *)
+      let val (is, os) = ExtendedIO.execute ("rm " ^ name)
+      in close_in is; close_out os end;
+
+    (*Get pathname of current working directory *)
+    fun getDir () =
+      let val (is, os) = ExtendedIO.execute ("pwd")
+	  val (path, _) = take_suffix (apr(op=,"\n")) (*remove newline*)
+			   (explode (ExtendedIO.input_line is)) 
+      in close_in is; close_out os; implode path end;
+
+    end
   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;
 
 
 (*** ML command execution ***)