wenzelm@4403: (* Title: Pure/ML-Systems/smlnj.ML wenzelm@4403: wenzelm@5708: Compatibility file for Standard ML of New Jersey 110 or later. wenzelm@4403: *) wenzelm@4403: wenzelm@28443: exception Interrupt; wenzelm@28443: wenzelm@24599: use "ML-Systems/proper_int.ML"; wenzelm@24599: use "ML-Systems/overloading_smlnj.ML"; wenzelm@23965: use "ML-Systems/exn.ML"; wenzelm@25732: use "ML-Systems/universal.ML"; wenzelm@28151: use "ML-Systems/thread_dummy.ML"; wenzelm@24688: use "ML-Systems/multithreading.ML"; wenzelm@26220: use "ML-Systems/system_shell.ML"; wenzelm@28268: use "ML-Systems/ml_name_space.ML"; wenzelm@23921: wenzelm@16542: wenzelm@16542: (*low-level pointer equality*) wenzelm@16502: wenzelm@21298: CM.autoload "$smlnj/init/init.cmi"; wenzelm@21298: val pointer_eq = InlineT.ptreql; paulson@16528: wenzelm@16502: wenzelm@4403: (* restore old-style character / string functions *) wenzelm@4403: wenzelm@24145: val ord = mk_int o SML90.ord; wenzelm@24145: val chr = SML90.chr o dest_int; paulson@10725: val explode = SML90.explode; paulson@10725: val implode = SML90.implode; wenzelm@4403: wenzelm@4403: wenzelm@4403: (* New Jersey ML parameters *) wenzelm@4403: wenzelm@4403: val _ = wenzelm@21298: (Control.Print.printLength := 1000; wenzelm@21298: Control.Print.printDepth := 350; wenzelm@21298: Control.Print.stringDepth := 250; wenzelm@21298: Control.Print.signatures := 2; wenzelm@21298: Control.MC.matchRedundantError := false); wenzelm@4403: wenzelm@4403: wenzelm@4403: (* Poly/ML emulation *) wenzelm@4403: wenzelm@24599: val exit = exit o dest_int; wenzelm@4403: fun quit () = exit 0; wenzelm@4403: wenzelm@4403: (*limit the printing depth -- divided by 2 for comparibility with Poly/ML*) wenzelm@24329: local wenzelm@24599: val depth = ref (10: int); wenzelm@24329: in wenzelm@24329: fun get_print_depth () = ! depth; wenzelm@24329: fun print_depth n = wenzelm@24329: (depth := n; wenzelm@24329: Control.Print.printDepth := dest_int n div 2; wenzelm@24329: Control.Print.printLength := dest_int n); wenzelm@24329: end; wenzelm@4403: wenzelm@26474: wenzelm@5816: (* compiler-independent timing functions *) wenzelm@4403: wenzelm@21298: fun start_timing () = wenzelm@30187: let wenzelm@30187: val timer = Timer.startCPUTimer (); wenzelm@30187: val time = Timer.checkCPUTimer timer; wenzelm@30187: in (timer, time) end; wenzelm@21298: wenzelm@30187: fun end_timing (timer, {sys, usr}) = wenzelm@30187: let wenzelm@30187: open Time; (*...for Time.toString, Time.+ and Time.- *) wenzelm@30187: val {sys = sys2, usr = usr2} = Timer.checkCPUTimer timer; wenzelm@30187: val user = usr2 - usr; wenzelm@30187: val all = user + sys2 - sys; wenzelm@30187: val message = "User " ^ toString user ^ " All "^ toString all ^ " secs" handle Time => ""; wenzelm@30187: in {message = message, user = user, all = all} end; wenzelm@21298: wenzelm@21298: fun check_timer timer = wenzelm@21298: let wenzelm@21298: val {sys, usr} = Timer.checkCPUTimer timer; wenzelm@21298: val gc = Timer.checkGCTime timer; (* FIXME already included in usr? *) wenzelm@21298: in (sys, usr, gc) end; wenzelm@4403: wenzelm@4403: wenzelm@16660: (*prompts*) wenzelm@4977: fun ml_prompts p1 p2 = wenzelm@21298: (Control.primaryPrompt := p1; Control.secondaryPrompt := p2); wenzelm@4977: wenzelm@17511: (*dummy implementation*) wenzelm@16681: fun profile (n: int) f x = f x; wenzelm@16681: wenzelm@17511: (*dummy implementation*) wenzelm@16681: fun exception_trace f = f (); wenzelm@4977: haftmann@18384: (*dummy implementation*) haftmann@18384: fun print x = x; wenzelm@16681: obua@23770: (*dummy implementation*) obua@23770: fun makestring x = "dummy string for SML New Jersey"; obua@23770: wenzelm@21298: wenzelm@24290: (* toplevel pretty printing (see also Pure/pure_setup.ML) *) wenzelm@4403: wenzelm@21298: fun make_pp path pprint = wenzelm@21298: let wenzelm@21298: open PrettyPrint; wenzelm@4403: wenzelm@21298: fun pp pps obj = wenzelm@21298: pprint obj wenzelm@24145: (string pps, openHOVBox pps o Rel o dest_int, wenzelm@24145: fn wd => break pps {nsp=dest_int wd, offset=0}, fn () => newline pps, wenzelm@21298: fn () => closeBox pps); wenzelm@21298: in (path, pp) end; wenzelm@21298: wenzelm@21298: fun install_pp (path, pp) = CompilerPPTable.install_pp path pp; wenzelm@4403: wenzelm@4403: wenzelm@4403: (* ML command execution *) wenzelm@4403: wenzelm@28268: fun use_text (tune: string -> string) _ _ (line: int, name) (print, err) verbose txt = wenzelm@5090: let wenzelm@21298: val ref out_orig = Control.Print.out; wenzelm@5090: wenzelm@5090: val out_buffer = ref ([]: string list); wenzelm@5090: val out = {say = (fn s => out_buffer := s :: ! out_buffer), flush = (fn () => ())}; wenzelm@10914: fun output () = wenzelm@7890: let val str = implode (rev (! out_buffer)) wenzelm@10914: in String.substring (str, 0, Int.max (0, size str - 1)) end; wenzelm@5090: in wenzelm@21298: Control.Print.out := out; wenzelm@24599: Backend.Interact.useStream (TextIO.openString (tune txt)) handle exn => wenzelm@22144: (Control.Print.out := out_orig; wenzelm@22144: err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn); wenzelm@21298: Control.Print.out := out_orig; wenzelm@10914: if verbose then print (output ()) else () wenzelm@5090: end; wenzelm@4403: wenzelm@28268: fun use_file tune str_of_pos name_space output verbose name = wenzelm@24599: let wenzelm@24599: val instream = TextIO.openIn name; wenzelm@26504: val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); wenzelm@28268: in use_text tune str_of_pos name_space (1, name) output verbose txt end; wenzelm@21770: wenzelm@26474: fun forget_structure name = wenzelm@28284: use_text (fn x => x) (fn _ => "") () (1, "ML") (TextIO.print, fn s => raise Fail s) false wenzelm@26474: ("structure " ^ name ^ " = struct end"); wenzelm@26474: wenzelm@21770: wenzelm@4403: wenzelm@5816: (** interrupts **) wenzelm@5816: wenzelm@26084: local wenzelm@26084: wenzelm@26084: fun change_signal new_handler f x = wenzelm@5816: let wenzelm@26084: val old_handler = Signals.setHandler (Signals.sigINT, new_handler); wenzelm@26084: val result = Exn.capture (f old_handler) x; wenzelm@12990: val _ = Signals.setHandler (Signals.sigINT, old_handler); wenzelm@23965: in Exn.release result end; wenzelm@5816: wenzelm@26084: in wenzelm@26084: wenzelm@26084: fun interruptible (f: 'a -> 'b) x = wenzelm@12990: let wenzelm@26084: val result = ref (Exn.Exn Interrupt: 'b Exn.result); wenzelm@12990: val old_handler = Signals.inqHandler Signals.sigINT; wenzelm@5816: in wenzelm@12990: SMLofNJ.Cont.callcc (fn cont => wenzelm@26084: (Signals.setHandler (Signals.sigINT, Signals.HANDLER (fn _ => cont)); wenzelm@26084: result := Exn.capture f x)); wenzelm@12990: Signals.setHandler (Signals.sigINT, old_handler); wenzelm@26084: Exn.release (! result) wenzelm@12990: end; wenzelm@5816: wenzelm@26084: fun uninterruptible f = wenzelm@26084: change_signal Signals.IGNORE wenzelm@26084: (fn old_handler => f (fn g => change_signal old_handler (fn _ => g))); wenzelm@26084: wenzelm@26084: end; wenzelm@26084: wenzelm@21298: wenzelm@21298: (* basis library fixes *) wenzelm@21298: wenzelm@21298: structure TextIO = wenzelm@21298: struct wenzelm@21298: open TextIO; wenzelm@23139: fun inputLine is = TextIO.inputLine is wenzelm@21298: handle IO.Io _ => raise Interrupt; wenzelm@21298: end; wenzelm@17511: webertj@18790: wenzelm@5816: wenzelm@4403: (** OS related **) wenzelm@4403: wenzelm@23826: (* current directory *) wenzelm@23826: wenzelm@23826: val cd = OS.FileSys.chDir; wenzelm@23826: val pwd = OS.FileSys.getDir; wenzelm@23826: wenzelm@23826: wenzelm@4403: (* system command execution *) wenzelm@4403: wenzelm@26220: val system_out = (fn (output, rc) => (output, mk_int rc)) o system_out; wenzelm@7855: wenzelm@4403: wenzelm@17824: (*Convert a process ID to a decimal string (chiefly for tracing)*) wenzelm@28488: fun process_id pid = wenzelm@28488: Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord (Posix.ProcEnv.getpid ()))); wenzelm@17824: wenzelm@17824: wenzelm@4403: (* getenv *) wenzelm@4403: wenzelm@4403: fun getenv var = wenzelm@4403: (case OS.Process.getEnv var of wenzelm@4403: NONE => "" wenzelm@4403: | SOME txt => txt);