# HG changeset patch # User wenzelm # Date 850122064 -3600 # Node ID 5b18cc02adb79e30b78149b11de53d0c691e82e7 # Parent 008ce88c9913f2416980c63e8b1ed55d1349dfc0 comitting symlinks failed!!! diff -r 008ce88c9913 -r 5b18cc02adb7 src/Pure/ML-Systems/polyml-2.07.ML --- 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; diff -r 008ce88c9913 -r 5b18cc02adb7 src/Pure/ML-Systems/polyml-3.1.ML --- 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;