# HG changeset patch # User wenzelm # Date 981380230 -3600 # Node ID 82578cdb76cfe8ccc9f0a55a8d7cafc14ce62a38 # Parent e86340dc1d2866cdf1ed254ebe2cb4a69a680d06 renamed polyml.ML to polyml-3.x.ML and polyml-4.0.ML to polyml.ML (default); diff -r e86340dc1d28 -r 82578cdb76cf src/Pure/ML-Systems/polyml-3.x.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML-Systems/polyml-3.x.ML Mon Feb 05 14:37:10 2001 +0100 @@ -0,0 +1,136 @@ +(* Title: Pure/ML-Systems/polyml.ML + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1991 University of Cambridge + +Compatibility file for Poly/ML (versions 2.x and 3.x). +*) + +open PolyML ExtendedIO; + +(*needs the Basis Library emulation*) +use "basis.ML"; + + +structure String = +struct + fun substring (s,i,j) = StringBuiltIns.substring (s, i+1, j) + handle Substring => raise Subscript + fun isPrefix s1 s2 = (s1 = substring(s2,0, size s1)) + handle Subscript => false +end; + + +(** ML system related **) + +(** Compiler-independent timing functions **) + +(*Note start point for timing*) +fun startTiming() = System.processtime (); + +(*Finish timing and return string*) +fun endTiming before = + "User + GC: " ^ + makestring (real (System.processtime () - before) / 10.0) ^ + " secs"; + + +(* prompts *) + +fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2); + + +(* toplevel pretty printing (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); + + +(* ML command execution -- 'eval' *) + +local + +fun drop_last [] = [] + | drop_last [x] = [] + | drop_last (x :: xs) = x :: drop_last xs; + +val drop_last_char = implode o drop_last o explode; + +in + +fun use_text (print, err) verbose txt = + let + val in_buffer = ref (explode txt); + val out_buffer = ref ([]: string list); + fun output () = drop_last_char (implode (rev (! out_buffer))); + + fun get () = + (case ! in_buffer of + [] => "" + | c :: cs => (in_buffer := cs; c)); + fun put s = out_buffer := s :: ! out_buffer; + + fun exec () = + (case ! in_buffer of + [] => () + | _ => (PolyML.compiler (get, put) (); exec ())); + in + exec () handle exn => (err (output ()); raise exn); + if verbose then print (output ()) else () + end; + + + +(** interrupts **) (*Note: may get into race conditions*) + +fun mask_interrupt f x = f x; +fun unmask_interrupt f x = f x; +fun exhibit_interrupt f x = f x; + + + +(** OS related **) + +(* system command execution *) + +(*execute 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 _ = close_out os; + val result = input (is, 999999); + in close_in is; result end; + +fun system cmd = (print (execute cmd); 0); (* FIXME rc not available *) + + +(* file handling *) + +(*get time of last modification*) +fun file_info name = Int.toString (System.filedate name) handle _ => ""; + +structure OS = +struct + structure FileSys = + struct + val chDir = PolyML.cd; + fun remove name = (execute ("rm " ^ name); ()); + fun getDir () = drop_last_char (execute "pwd"); + end; +end; + + +(* getenv *) + +fun getenv var = drop_last_char + (execute ("env | grep '^" ^ var ^ "=' | sed -e 's/" ^ var ^ "=//'")); + + +end; + + +(* non-ASCII input (see also Thy/use.ML) *) + +val needs_filtered_use = true; diff -r e86340dc1d28 -r 82578cdb76cf src/Pure/ML-Systems/polyml-4.0.ML --- a/src/Pure/ML-Systems/polyml-4.0.ML Mon Feb 05 14:31:49 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,174 +0,0 @@ -(* Title: Pure/ML-Systems/polyml.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1991 University of Cambridge - -Compatibility file for Poly/ML (version 4.0). -*) - -(** ML system related **) - -(* old Poly/ML emulation *) - -local - val orig_exit = exit; -in - open PolyML; - val exit = orig_exit; - fun quit () = exit 0; -end; - - -(* restore old-style character / string functions *) - -val ord = SML90.ord; -val chr = SML90.chr; -val explode = SML90.explode; -val implode = SML90.implode; - - -(*Note start point for timing*) -fun startTiming() = - let val CPUtimer = Timer.startCPUTimer(); - val time = Timer.checkCPUTimer(CPUtimer) - in (CPUtimer,time) end; - -(*Finish timing and return string*) -fun endTiming (CPUtimer, {sys,usr}) = - let open Time (*...for Time.toString, Time.+ and Time.- *) - val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer) - in "User " ^ toString (usr2-usr) ^ - " All "^ toString (sys2-sys + usr2-usr) ^ - " secs" - handle Time => "" - end; - - -(* prompts *) - -fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2); - - -(* toplevel pretty printing (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); - - -(* ML command execution -- 'eval' *) - -local - -fun drop_last [] = [] - | drop_last [x] = [] - | drop_last (x :: xs) = x :: drop_last xs; - -val drop_last_char = implode o drop_last o explode; - -in - -fun use_text (print, err) verbose txt = - let - val in_buffer = ref (explode txt); - val out_buffer = ref ([]: string list); - fun output () = drop_last_char (implode (rev (! out_buffer))); - - fun get () = - (case ! in_buffer of - [] => "" - | c :: cs => (in_buffer := cs; c)); - fun put s = out_buffer := s :: ! out_buffer; - - fun exec () = - (case ! in_buffer of - [] => () - | _ => (PolyML.compiler (get, put) (); exec ())); - in - exec () handle exn => (err (output ()); raise exn); - if verbose then print (output ()) else () - end; - -end; - - - -(** interrupts **) - -exception Interrupt = SML90.Interrupt; - -local - -datatype 'a result = - Result of 'a | - Exn of exn; - -fun capture f x = Result (f x) handle exn => Exn exn; - -fun release (Result x) = x - | release (Exn exn) = raise exn; - - -val sig_int = 2; - -fun change_signal new_handler f x = - let - (*RACE wrt. other signals*) - val old_handler = Signal.signal (sig_int, new_handler); - val result = capture f x; - val _ = Signal.signal (sig_int, old_handler); - in release result end; - -val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ()); - -in - -val _ = Signal.signal (sig_int, default_handler); - -fun mask_interrupt f = change_signal Signal.SIG_IGN f; -fun exhibit_interrupt f = change_signal default_handler f; - -end; - - - -(** OS related **) - -(* system command execution *) - -(*execute Unix command which doesn't take any input from stdin and - sends its output to stdout; could be done more easily by Unix.execute, - but that function doesn't use the PATH*) -fun execute command = - let - val tmp_name = OS.FileSys.tmpName (); - val is = (OS.Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name); - val result = TextIO.inputAll is; - in - TextIO.closeIn is; - OS.FileSys.remove tmp_name; - result - end; - -(*plain version; with return code*) -fun system cmd = - if OS.Process.isSuccess (OS.Process.system cmd) then 0 else 1; - - -(* file handling *) - -(*get time of last modification*) -fun file_info name = Time.toString (OS.FileSys.modTime name) handle _ => ""; - - -(* getenv *) - -fun getenv var = - (case OS.Process.getEnv var of - NONE => "" - | SOME txt => txt); - - -(* non-ASCII input (see also Thy/use.ML) *) - -val needs_filtered_use = true;