# HG changeset patch # User paulson # Date 849087958 -3600 # Node ID fa8c6c695a9776d2641ca7a200e104ae4685d60b # Parent cc5ee79ea4165c6759caf14d645ed36828c0da40 Basis library emulation, especially of I/O operations diff -r cc5ee79ea416 -r fa8c6c695a97 src/Pure/NJ093.ML --- 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")); diff -r cc5ee79ea416 -r fa8c6c695a97 src/Pure/POLY.ML --- 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 ***)