| author | wenzelm | 
| Tue, 20 Oct 2009 21:22:37 +0200 | |
| changeset 33030 | 2f4b36efa95e | 
| parent 32776 | 1504f9c2d060 | 
| child 33060 | e66b41782cb5 | 
| permissions | -rw-r--r-- | 
| 4403 | 1 | (* Title: Pure/ML-Systems/smlnj.ML | 
| 2 | ||
| 5708 | 3 | Compatibility file for Standard ML of New Jersey 110 or later. | 
| 4403 | 4 | *) | 
| 5 | ||
| 28443 | 6 | exception Interrupt; | 
| 31427 
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
 wenzelm parents: 
31321diff
changeset | 7 | fun reraise exn = raise exn; | 
| 28443 | 8 | |
| 24599 
7b0ecf9a9055
use_text/file: tune text (cf. ML_Parse.fix_ints);
 wenzelm parents: 
24329diff
changeset | 9 | use "ML-Systems/proper_int.ML"; | 
| 32776 
1504f9c2d060
more uniform treatment of structure Unsynchronized in ML bootstrap phase;
 wenzelm parents: 
32737diff
changeset | 10 | use "ML-Systems/unsynchronized.ML"; | 
| 24599 
7b0ecf9a9055
use_text/file: tune text (cf. ML_Parse.fix_ints);
 wenzelm parents: 
24329diff
changeset | 11 | use "ML-Systems/overloading_smlnj.ML"; | 
| 23965 
f93e509659c1
ML-Systems/exn.ML, ML-Systems/multithreading_dummy.ML;
 wenzelm parents: 
23921diff
changeset | 12 | use "ML-Systems/exn.ML"; | 
| 25732 | 13 | use "ML-Systems/universal.ML"; | 
| 28151 
61f9c918b410
explicit use of universal.ML and dummy_thread.ML;
 wenzelm parents: 
26885diff
changeset | 14 | use "ML-Systems/thread_dummy.ML"; | 
| 24688 
a5754ca5c510
replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
 wenzelm parents: 
24599diff
changeset | 15 | use "ML-Systems/multithreading.ML"; | 
| 31686 
e54ae15335a1
more detailed start_timing/end_timing (in timing.ML);
 wenzelm parents: 
31427diff
changeset | 16 | use "ML-Systems/timing.ML"; | 
| 26220 | 17 | use "ML-Systems/system_shell.ML"; | 
| 28268 
ac8431ecd57e
use_text/use_file now depend on explicit ML name space;
 wenzelm parents: 
28151diff
changeset | 18 | use "ML-Systems/ml_name_space.ML"; | 
| 30619 | 19 | use "ML-Systems/ml_pretty.ML"; | 
| 30672 
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
 wenzelm parents: 
30626diff
changeset | 20 | use "ML-Systems/use_context.ML"; | 
| 23921 
947152add153
added compatibility file for ML systems without multithreading;
 wenzelm parents: 
23826diff
changeset | 21 | |
| 16542 | 22 | |
| 23 | (*low-level pointer equality*) | |
| 16502 | 24 | |
| 21298 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
 wenzelm parents: 
18790diff
changeset | 25 | CM.autoload "$smlnj/init/init.cmi"; | 
| 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
 wenzelm parents: 
18790diff
changeset | 26 | val pointer_eq = InlineT.ptreql; | 
| 16528 | 27 | |
| 16502 | 28 | |
| 4403 | 29 | (* restore old-style character / string functions *) | 
| 30 | ||
| 24145 | 31 | val ord = mk_int o SML90.ord; | 
| 32 | val chr = SML90.chr o dest_int; | |
| 10725 | 33 | val explode = SML90.explode; | 
| 34 | val implode = SML90.implode; | |
| 4403 | 35 | |
| 36 | ||
| 37 | (* New Jersey ML parameters *) | |
| 38 | ||
| 39 | val _ = | |
| 21298 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
 wenzelm parents: 
18790diff
changeset | 40 | (Control.Print.printLength := 1000; | 
| 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
 wenzelm parents: 
18790diff
changeset | 41 | Control.Print.printDepth := 350; | 
| 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
 wenzelm parents: 
18790diff
changeset | 42 | Control.Print.stringDepth := 250; | 
| 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
 wenzelm parents: 
18790diff
changeset | 43 | Control.Print.signatures := 2; | 
| 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
 wenzelm parents: 
18790diff
changeset | 44 | Control.MC.matchRedundantError := false); | 
| 4403 | 45 | |
| 46 | ||
| 47 | (* Poly/ML emulation *) | |
| 48 | ||
| 24599 
7b0ecf9a9055
use_text/file: tune text (cf. ML_Parse.fix_ints);
 wenzelm parents: 
24329diff
changeset | 49 | val exit = exit o dest_int; | 
| 4403 | 50 | fun quit () = exit 0; | 
| 51 | ||
| 52 | (*limit the printing depth -- divided by 2 for comparibility with Poly/ML*) | |
| 24329 | 53 | local | 
| 24599 
7b0ecf9a9055
use_text/file: tune text (cf. ML_Parse.fix_ints);
 wenzelm parents: 
24329diff
changeset | 54 | val depth = ref (10: int); | 
| 24329 | 55 | in | 
| 56 | fun get_print_depth () = ! depth; | |
| 57 | fun print_depth n = | |
| 58 | (depth := n; | |
| 59 | Control.Print.printDepth := dest_int n div 2; | |
| 60 | Control.Print.printLength := dest_int n); | |
| 61 | end; | |
| 4403 | 62 | |
| 26474 | 63 | |
| 16660 | 64 | (*prompts*) | 
| 4977 | 65 | fun ml_prompts p1 p2 = | 
| 21298 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
 wenzelm parents: 
18790diff
changeset | 66 | (Control.primaryPrompt := p1; Control.secondaryPrompt := p2); | 
| 4977 | 67 | |
| 17511 | 68 | (*dummy implementation*) | 
| 16681 | 69 | fun profile (n: int) f x = f x; | 
| 70 | ||
| 17511 | 71 | (*dummy implementation*) | 
| 16681 | 72 | fun exception_trace f = f (); | 
| 4977 | 73 | |
| 21298 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
 wenzelm parents: 
18790diff
changeset | 74 | |
| 4403 | 75 | (* ML command execution *) | 
| 76 | ||
| 30672 
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
 wenzelm parents: 
30626diff
changeset | 77 | fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
 | 
| 5090 | 78 | let | 
| 21298 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
 wenzelm parents: 
18790diff
changeset | 79 | val ref out_orig = Control.Print.out; | 
| 5090 | 80 | |
| 81 | val out_buffer = ref ([]: string list); | |
| 82 |     val out = {say = (fn s => out_buffer := s :: ! out_buffer), flush = (fn () => ())};
 | |
| 10914 | 83 | fun output () = | 
| 7890 | 84 | let val str = implode (rev (! out_buffer)) | 
| 10914 | 85 | in String.substring (str, 0, Int.max (0, size str - 1)) end; | 
| 5090 | 86 | in | 
| 21298 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
 wenzelm parents: 
18790diff
changeset | 87 | Control.Print.out := out; | 
| 30672 
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
 wenzelm parents: 
30626diff
changeset | 88 | Backend.Interact.useStream (TextIO.openString (tune_source txt)) handle exn => | 
| 22144 | 89 | (Control.Print.out := out_orig; | 
| 30672 
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
 wenzelm parents: 
30626diff
changeset | 90 | error ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn); | 
| 21298 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
 wenzelm parents: 
18790diff
changeset | 91 | Control.Print.out := out_orig; | 
| 10914 | 92 | if verbose then print (output ()) else () | 
| 5090 | 93 | end; | 
| 4403 | 94 | |
| 30672 
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
 wenzelm parents: 
30626diff
changeset | 95 | fun use_file context verbose name = | 
| 24599 
7b0ecf9a9055
use_text/file: tune text (cf. ML_Parse.fix_ints);
 wenzelm parents: 
24329diff
changeset | 96 | let | 
| 
7b0ecf9a9055
use_text/file: tune text (cf. ML_Parse.fix_ints);
 wenzelm parents: 
24329diff
changeset | 97 | val instream = TextIO.openIn name; | 
| 26504 | 98 | val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); | 
| 30672 
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
 wenzelm parents: 
30626diff
changeset | 99 | in use_text context (1, name) verbose txt end; | 
| 21770 | 100 | |
| 30672 
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
 wenzelm parents: 
30626diff
changeset | 101 | fun forget_structure _ = (); | 
| 26474 | 102 | |
| 21770 | 103 | |
| 30626 | 104 | (* toplevel pretty printing *) | 
| 105 | ||
| 106 | fun ml_pprint pps = | |
| 107 | let | |
| 108 | fun str "" = () | |
| 109 | | str s = PrettyPrint.string pps s; | |
| 110 | fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) = | |
| 111 | (str bg; PrettyPrint.openHOVBox pps (PrettyPrint.Rel (dest_int ind)); | |
| 112 | List.app pprint prts; PrettyPrint.closeBox pps; str en) | |
| 113 | | pprint (ML_Pretty.String (s, _)) = str s | |
| 114 |       | pprint (ML_Pretty.Break (false, wd)) = PrettyPrint.break pps {nsp = dest_int wd, offset = 0}
 | |
| 115 | | pprint (ML_Pretty.Break (true, _)) = PrettyPrint.newline pps; | |
| 116 | in pprint end; | |
| 117 | ||
| 30672 
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
 wenzelm parents: 
30626diff
changeset | 118 | fun toplevel_pp context path pp = | 
| 
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
 wenzelm parents: 
30626diff
changeset | 119 | use_text context (1, "pp") false | 
| 30626 | 120 |     ("CompilerPPTable.install_pp [" ^ String.concatWith "," (map (fn s => "\"" ^ s ^ "\"")  path) ^
 | 
| 121 |       "] (fn pps => ml_pprint pps o Pretty.to_ML o (" ^ pp ^ "))");
 | |
| 122 | ||
| 123 | ||
| 4403 | 124 | |
| 5816 | 125 | (** interrupts **) | 
| 126 | ||
| 26084 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
 wenzelm parents: 
25732diff
changeset | 127 | local | 
| 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
 wenzelm parents: 
25732diff
changeset | 128 | |
| 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
 wenzelm parents: 
25732diff
changeset | 129 | fun change_signal new_handler f x = | 
| 5816 | 130 | let | 
| 26084 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
 wenzelm parents: 
25732diff
changeset | 131 | val old_handler = Signals.setHandler (Signals.sigINT, new_handler); | 
| 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
 wenzelm parents: 
25732diff
changeset | 132 | val result = Exn.capture (f old_handler) x; | 
| 12990 | 133 | val _ = Signals.setHandler (Signals.sigINT, old_handler); | 
| 23965 
f93e509659c1
ML-Systems/exn.ML, ML-Systems/multithreading_dummy.ML;
 wenzelm parents: 
23921diff
changeset | 134 | in Exn.release result end; | 
| 5816 | 135 | |
| 26084 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
 wenzelm parents: 
25732diff
changeset | 136 | in | 
| 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
 wenzelm parents: 
25732diff
changeset | 137 | |
| 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
 wenzelm parents: 
25732diff
changeset | 138 | fun interruptible (f: 'a -> 'b) x = | 
| 12990 | 139 | let | 
| 26084 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
 wenzelm parents: 
25732diff
changeset | 140 | val result = ref (Exn.Exn Interrupt: 'b Exn.result); | 
| 12990 | 141 | val old_handler = Signals.inqHandler Signals.sigINT; | 
| 5816 | 142 | in | 
| 12990 | 143 | SMLofNJ.Cont.callcc (fn cont => | 
| 26084 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
 wenzelm parents: 
25732diff
changeset | 144 | (Signals.setHandler (Signals.sigINT, Signals.HANDLER (fn _ => cont)); | 
| 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
 wenzelm parents: 
25732diff
changeset | 145 | result := Exn.capture f x)); | 
| 12990 | 146 | Signals.setHandler (Signals.sigINT, old_handler); | 
| 26084 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
 wenzelm parents: 
25732diff
changeset | 147 | Exn.release (! result) | 
| 12990 | 148 | end; | 
| 5816 | 149 | |
| 26084 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
 wenzelm parents: 
25732diff
changeset | 150 | fun uninterruptible f = | 
| 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
 wenzelm parents: 
25732diff
changeset | 151 | change_signal Signals.IGNORE | 
| 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
 wenzelm parents: 
25732diff
changeset | 152 | (fn old_handler => f (fn g => change_signal old_handler (fn _ => g))); | 
| 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
 wenzelm parents: 
25732diff
changeset | 153 | |
| 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
 wenzelm parents: 
25732diff
changeset | 154 | end; | 
| 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
 wenzelm parents: 
25732diff
changeset | 155 | |
| 21298 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
 wenzelm parents: 
18790diff
changeset | 156 | |
| 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
 wenzelm parents: 
18790diff
changeset | 157 | (* basis library fixes *) | 
| 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
 wenzelm parents: 
18790diff
changeset | 158 | |
| 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
 wenzelm parents: 
18790diff
changeset | 159 | structure TextIO = | 
| 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
 wenzelm parents: 
18790diff
changeset | 160 | struct | 
| 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
 wenzelm parents: 
18790diff
changeset | 161 | open TextIO; | 
| 23139 
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
 wenzelm parents: 
22144diff
changeset | 162 | fun inputLine is = TextIO.inputLine is | 
| 21298 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
 wenzelm parents: 
18790diff
changeset | 163 | handle IO.Io _ => raise Interrupt; | 
| 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
 wenzelm parents: 
18790diff
changeset | 164 | end; | 
| 17511 | 165 | |
| 18790 
418131f631fc
interrupt_timeout now raises Interrupt instead of SML90.Interrupt
 webertj parents: 
18760diff
changeset | 166 | |
| 5816 | 167 | |
| 4403 | 168 | (** OS related **) | 
| 169 | ||
| 23826 
463903573934
moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
 wenzelm parents: 
23770diff
changeset | 170 | (* current directory *) | 
| 
463903573934
moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
 wenzelm parents: 
23770diff
changeset | 171 | |
| 
463903573934
moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
 wenzelm parents: 
23770diff
changeset | 172 | val cd = OS.FileSys.chDir; | 
| 
463903573934
moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
 wenzelm parents: 
23770diff
changeset | 173 | val pwd = OS.FileSys.getDir; | 
| 
463903573934
moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
 wenzelm parents: 
23770diff
changeset | 174 | |
| 
463903573934
moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
 wenzelm parents: 
23770diff
changeset | 175 | |
| 4403 | 176 | (* system command execution *) | 
| 177 | ||
| 26220 | 178 | val system_out = (fn (output, rc) => (output, mk_int rc)) o system_out; | 
| 7855 | 179 | |
| 4403 | 180 | |
| 17824 | 181 | (*Convert a process ID to a decimal string (chiefly for tracing)*) | 
| 28488 
18fea7e88ea1
removed obsolete Posix/Signal compatibility wrappers;
 wenzelm parents: 
28443diff
changeset | 182 | fun process_id pid = | 
| 
18fea7e88ea1
removed obsolete Posix/Signal compatibility wrappers;
 wenzelm parents: 
28443diff
changeset | 183 | Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord (Posix.ProcEnv.getpid ()))); | 
| 17824 | 184 | |
| 185 | ||
| 4403 | 186 | (* getenv *) | 
| 187 | ||
| 188 | fun getenv var = | |
| 189 | (case OS.Process.getEnv var of | |
| 190 | NONE => "" | |
| 191 | | SOME txt => txt); |