--- a/src/Pure/ML-Systems/polyml-2.07.ML Mon Dec 09 09:59:43 1996 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,123 +0,0 @@
-(* Title: Pure/POLY
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
-
-Compatibility file for Poly/ML (AHL release 1.88)
-*)
-
-open PolyML ExtendedIO;
-
-use"basis.ML";
-
-(*A conditional timing function: applies f to () and, if the flag is true,
- prints its runtime.*)
-
-fun cond_timeit flag f =
- if flag then
- let val before = System.processtime()
- val result = f()
- val both = real(System.processtime() - before) / 10.0
- in output(std_out, "Process time (incl GC): "^
- makestring both ^ " secs\n");
- result
- end
- else f();
-
-
-(*Save function: in Poly/ML, ignores filename and commits to present file*)
-
-fun xML filename banner = commit();
-
-
-(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
-
-fun make_pp _ pprint (str, blk, brk, en) obj =
- pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
- fn () => brk (99999, 0), en);
-
-
-(*** 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);
-
-fun seq (proc: 'a -> unit) : 'a list -> unit =
- let fun seqf [] = ()
- | seqf (x :: xs) = (proc x; seqf xs)
- in seqf end;
-
-fun radixpand num : int list =
- let fun radix (n, tail) =
- if n < 10 then n :: tail else radix (n div 10, (n mod 10) :: tail)
- in radix (num, []) end;
-
-fun radixstring num =
- let fun chrof n = chr (ord "0" + n);
- in implode (map chrof (radixpand num)) end;
-
-in
-
-(*Get time of last modification; if file doesn't exist return an empty string*)
-fun file_info "" = ""
- | file_info name = radixstring (System.filedate name) handle _ => "";
-
-
-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;
-
-
-
-(*** ML command execution ***)
-
-val use_string =
- let fun exec command =
- let val firstLine = ref true;
-
- fun getLine () =
- if !firstLine
- then (firstLine := false; command)
- else raise Io "use_string: buffer exhausted"
- in PolyML.compiler (getLine, fn s => output (std_out, s)) () end
- in seq exec end;
-
-end;
-
-
-(*** System command execution ***)
-
-(*Execute an Unix command which doesn't take any input from stdin and
- sends its output to stdout.*)
-fun execute command =
- let val (is, os) = ExtendedIO.execute command;
- val result = input (is, 999999);
- in close_out os;
- close_in is;
- result
- end;
--- a/src/Pure/ML-Systems/polyml-3.1.ML Mon Dec 09 09:59:43 1996 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,123 +0,0 @@
-(* Title: Pure/POLY
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
-
-Compatibility file for Poly/ML (AHL release 1.88)
-*)
-
-open PolyML ExtendedIO;
-
-use"basis.ML";
-
-(*A conditional timing function: applies f to () and, if the flag is true,
- prints its runtime.*)
-
-fun cond_timeit flag f =
- if flag then
- let val before = System.processtime()
- val result = f()
- val both = real(System.processtime() - before) / 10.0
- in output(std_out, "Process time (incl GC): "^
- makestring both ^ " secs\n");
- result
- end
- else f();
-
-
-(*Save function: in Poly/ML, ignores filename and commits to present file*)
-
-fun xML filename banner = commit();
-
-
-(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
-
-fun make_pp _ pprint (str, blk, brk, en) obj =
- pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
- fn () => brk (99999, 0), en);
-
-
-(*** 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);
-
-fun seq (proc: 'a -> unit) : 'a list -> unit =
- let fun seqf [] = ()
- | seqf (x :: xs) = (proc x; seqf xs)
- in seqf end;
-
-fun radixpand num : int list =
- let fun radix (n, tail) =
- if n < 10 then n :: tail else radix (n div 10, (n mod 10) :: tail)
- in radix (num, []) end;
-
-fun radixstring num =
- let fun chrof n = chr (ord "0" + n);
- in implode (map chrof (radixpand num)) end;
-
-in
-
-(*Get time of last modification; if file doesn't exist return an empty string*)
-fun file_info "" = ""
- | file_info name = radixstring (System.filedate name) handle _ => "";
-
-
-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;
-
-
-
-(*** ML command execution ***)
-
-val use_string =
- let fun exec command =
- let val firstLine = ref true;
-
- fun getLine () =
- if !firstLine
- then (firstLine := false; command)
- else raise Io "use_string: buffer exhausted"
- in PolyML.compiler (getLine, fn s => output (std_out, s)) () end
- in seq exec end;
-
-end;
-
-
-(*** System command execution ***)
-
-(*Execute an Unix command which doesn't take any input from stdin and
- sends its output to stdout.*)
-fun execute command =
- let val (is, os) = ExtendedIO.execute command;
- val result = input (is, 999999);
- in close_out os;
- close_in is;
- result
- end;