author | wenzelm |
Mon, 01 Jun 2009 15:25:59 +0200 | |
changeset 31324 | 3ffa005c7701 |
parent 31319 | 6974449ddea9 |
child 31686 | e54ae15335a1 |
permissions | -rw-r--r-- |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ML-Systems/polyml_common.ML |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
2 |
|
31308 | 3 |
Compatibility file for Poly/ML -- common part for 5.x. |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
4 |
*) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
5 |
|
28443 | 6 |
exception Interrupt = SML90.Interrupt; |
7 |
||
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
8 |
use "ML-Systems/exn.ML"; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
9 |
use "ML-Systems/multithreading.ML"; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
10 |
use "ML-Systems/time_limit.ML"; |
26220 | 11 |
use "ML-Systems/system_shell.ML"; |
30619 | 12 |
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:
30625
diff
changeset
|
13 |
use "ML-Systems/use_context.ML"; |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
14 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
15 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
16 |
(** ML system and platform related **) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
17 |
|
26474 | 18 |
val forget_structure = PolyML.Compiler.forgetStructure; |
19 |
||
31324
3ffa005c7701
removed print function from global ML name space, to reduce risk of surprises;
wenzelm
parents:
31319
diff
changeset
|
20 |
val _ = PolyML.Compiler.forgetValue "print"; |
3ffa005c7701
removed print function from global ML name space, to reduce risk of surprises;
wenzelm
parents:
31319
diff
changeset
|
21 |
|
26474 | 22 |
|
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
23 |
(* Compiler options *) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
24 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
25 |
val ml_system_fix_ints = false; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
26 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
27 |
PolyML.Compiler.printInAlphabeticalOrder := false; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
28 |
PolyML.Compiler.maxInlineSize := 80; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
29 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
30 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
31 |
(* old Poly/ML emulation *) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
32 |
|
31319
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
33 |
fun quit () = exit 0; |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
34 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
35 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
36 |
(* restore old-style character / string functions *) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
37 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
38 |
val ord = SML90.ord; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
39 |
val chr = SML90.chr; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
40 |
val explode = SML90.explode; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
41 |
val implode = SML90.implode; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
42 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
43 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
44 |
(* compiler-independent timing functions *) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
45 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
46 |
fun start_timing () = |
30187
b92b3375e919
end_timing: generalized result -- message plus with explicit time values;
wenzelm
parents:
29564
diff
changeset
|
47 |
let |
b92b3375e919
end_timing: generalized result -- message plus with explicit time values;
wenzelm
parents:
29564
diff
changeset
|
48 |
val timer = Timer.startCPUTimer (); |
b92b3375e919
end_timing: generalized result -- message plus with explicit time values;
wenzelm
parents:
29564
diff
changeset
|
49 |
val time = Timer.checkCPUTimer timer; |
b92b3375e919
end_timing: generalized result -- message plus with explicit time values;
wenzelm
parents:
29564
diff
changeset
|
50 |
in (timer, time) end; |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
51 |
|
30187
b92b3375e919
end_timing: generalized result -- message plus with explicit time values;
wenzelm
parents:
29564
diff
changeset
|
52 |
fun end_timing (timer, {sys, usr}) = |
b92b3375e919
end_timing: generalized result -- message plus with explicit time values;
wenzelm
parents:
29564
diff
changeset
|
53 |
let |
b92b3375e919
end_timing: generalized result -- message plus with explicit time values;
wenzelm
parents:
29564
diff
changeset
|
54 |
open Time; (*...for Time.toString, Time.+ and Time.- *) |
b92b3375e919
end_timing: generalized result -- message plus with explicit time values;
wenzelm
parents:
29564
diff
changeset
|
55 |
val {sys = sys2, usr = usr2} = Timer.checkCPUTimer timer; |
b92b3375e919
end_timing: generalized result -- message plus with explicit time values;
wenzelm
parents:
29564
diff
changeset
|
56 |
val user = usr2 - usr; |
b92b3375e919
end_timing: generalized result -- message plus with explicit time values;
wenzelm
parents:
29564
diff
changeset
|
57 |
val all = user + sys2 - sys; |
b92b3375e919
end_timing: generalized result -- message plus with explicit time values;
wenzelm
parents:
29564
diff
changeset
|
58 |
val message = "User " ^ toString user ^ " All "^ toString all ^ " secs" handle Time => ""; |
b92b3375e919
end_timing: generalized result -- message plus with explicit time values;
wenzelm
parents:
29564
diff
changeset
|
59 |
in {message = message, user = user, all = all} end; |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
60 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
61 |
fun check_timer timer = |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
62 |
let |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
63 |
val {sys, usr} = Timer.checkCPUTimer timer; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
64 |
val gc = Timer.checkGCTime timer; (* FIXME already included in usr? *) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
65 |
in (sys, usr, gc) end; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
66 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
67 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
68 |
(* prompts *) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
69 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
70 |
fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2); |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
71 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
72 |
|
30625
d53d1a16d5ee
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents:
30619
diff
changeset
|
73 |
(* print depth *) |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
74 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
75 |
local |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
76 |
val depth = ref 10; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
77 |
in |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
78 |
fun get_print_depth () = ! depth; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
79 |
fun print_depth n = (depth := n; PolyML.print_depth n); |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
80 |
end; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
81 |
|
31319
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
82 |
val error_depth = PolyML.error_depth; |
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
83 |
|
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
84 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
85 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
86 |
(** interrupts **) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
87 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
88 |
local |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
89 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
90 |
val sig_int = 2; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
91 |
val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ()); |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
92 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
93 |
val _ = Signal.signal (sig_int, default_handler); |
26380
5d368eb42c11
removed pointer_eq from polyml_common.ML (structure Address no longer available after 5.1);
wenzelm
parents:
26220
diff
changeset
|
94 |
val _ = PolyML.onEntry (fn () => (Signal.signal (sig_int, default_handler); ())); |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
95 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
96 |
fun change_signal new_handler f x = |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
97 |
let |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
98 |
(*RACE wrt. other signals!*) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
99 |
val old_handler = Signal.signal (sig_int, new_handler); |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
100 |
val result = Exn.capture (f old_handler) x; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
101 |
val _ = Signal.signal (sig_int, old_handler); |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
102 |
in Exn.release result end; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
103 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
104 |
in |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
105 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
106 |
fun interruptible f = change_signal default_handler (fn _ => f); |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
107 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
108 |
fun uninterruptible f = |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
109 |
change_signal Signal.SIG_IGN |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
110 |
(fn old_handler => f (fn g => change_signal old_handler (fn _ => g))); |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
111 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
112 |
end; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
113 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
114 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
115 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
116 |
(** OS related **) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
117 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
118 |
(* current directory *) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
119 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
120 |
val cd = OS.FileSys.chDir; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
121 |
val pwd = OS.FileSys.getDir; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
122 |
|
28488
18fea7e88ea1
removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents:
28443
diff
changeset
|
123 |
fun process_id () = |
18fea7e88ea1
removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents:
28443
diff
changeset
|
124 |
Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord (Posix.ProcEnv.getpid ()))); |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
125 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
126 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
127 |
(* getenv *) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
128 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
129 |
fun getenv var = |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
130 |
(case OS.Process.getEnv var of |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
131 |
NONE => "" |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
132 |
| SOME txt => txt); |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
133 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
134 |
|
31319
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
135 |
|
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
136 |
(** Runtime system **) |
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
137 |
|
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
138 |
val exception_trace = PolyML.exception_trace; |
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
139 |
val timing = PolyML.timing; |
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
140 |
val profiling = PolyML.profiling; |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
141 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
142 |
fun profile 0 f x = f x |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
143 |
| profile n f x = |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
144 |
let |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
145 |
val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
146 |
val res = Exn.capture f x; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
147 |
val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
148 |
in Exn.release res end; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
149 |