(* Title: Pure/ML-Systems/smlnj.ML Author: Carsten Clasohm and Markus Wenzel, TU Muenchen Compatibility file for Standard ML of New Jersey versions 110.72. *) (** ML system related **) (* restore old-style character / string functions *) fun ord s = Char.ord (String.sub (s, 0)); val chr = str o Char.chr; val explode = (map str) o String.explode; val implode = String.concat; (* New Jersey ML parameters *) structure Compiler = struct open Compiler; structure Control = Control; structure PrettyPrint = PrettyPrint; structure PPTable = CompilerPPTable; structure Interact = Backend.Interact; end; val _ = (Compiler.Control.Print.printLength := 1000; Compiler.Control.Print.printDepth := 350; Compiler.Control.Print.stringDepth := 250; Compiler.Control.Print.signatures := 2); (* interrupts *) exception Interrupt; local fun capture f x = ((f x): unit; NONE) handle exn => SOME exn; fun release NONE = () | release (SOME exn) = raise exn; in fun ignore_interrupt f x = let val old_handler = Signals.setHandler (Signals.sigINT, Signals.IGNORE); val result = capture f x; val _ = Signals.setHandler (Signals.sigINT, old_handler); in release result end; fun raise_interrupt f x = let val interrupted = ref false; val result = ref NONE; val old_handler = Signals.inqHandler Signals.sigINT; in SMLofNJ.Cont.callcc (fn cont => (Signals.setHandler (Signals.sigINT, Signals.HANDLER (fn _ => (interrupted := true; cont))); result := capture f x)); Signals.setHandler (Signals.sigINT, old_handler); if ! interrupted then raise Interrupt else release (! result) end; end; (* basis library incompatibilities *) structure TextIO = struct open TextIO; fun inputLine is = (case TextIO.inputLine is of SOME str => str | NONE => "") handle IO.Io _ => raise Interrupt; end; (* Poly/ML emulation *) fun quit () = exit 0; (*limit the printing depth -- divided by 2 for comparibility with Poly/ML*) fun print_depth n = (Compiler.Control.Print.printDepth := n div 2; Compiler.Control.Print.printLength := n); (*Poly/ML-like prompts*) Compiler.Control.primaryPrompt := "> "; Compiler.Control.secondaryPrompt := "# "; (** Compiler-independent timing functions **) (*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; fun checkTimer timer = let val {sys, usr} = Timer.checkCPUTimer timer; val gc = Timer.checkGCTime timer; (* FIXME already included in usr? *) in (sys, usr, gc) end; (* toplevel pretty printing (see also Pure/install_pp.ML) *) fun make_pp path pprint = let open Compiler.PrettyPrint; fun pp pps obj = pprint obj (string pps, openHOVBox pps o Rel, fn wd => break pps {nsp=wd, offset=0}, fn () => newline pps, fn () => closeBox pps); in (path, pp) end; fun install_pp (path, pp) = Compiler.PPTable.install_pp path pp; (* ML command execution *) val use_strings = Compiler.Interact.useStream o TextIO.openString o implode; (** 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; (* file handling *) (*get time of last modification; if file doesn't exist return an empty string*) fun file_info "" = "" (* FIXME !? *) | 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 = false;