author | blanchet |
Wed, 02 Jun 2010 15:18:48 +0200 | |
changeset 37321 | 9d7cfae95b30 |
parent 36876 | 1abc27d6c362 |
child 39585 | 00be8711082f |
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 |
||
34136 | 8 |
use "General/exn.ML"; |
36876 | 9 |
|
10 |
if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ()) |
|
11 |
then () |
|
12 |
else use "ML-Systems/single_assignment_polyml.ML"; |
|
13 |
||
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
14 |
use "ML-Systems/multithreading.ML"; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
15 |
use "ML-Systems/time_limit.ML"; |
31686
e54ae15335a1
more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
31324
diff
changeset
|
16 |
use "ML-Systems/timing.ML"; |
35010
d6e492cea6e4
renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents:
34136
diff
changeset
|
17 |
use "ML-Systems/bash.ML"; |
30619 | 18 |
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
|
19 |
use "ML-Systems/use_context.ML"; |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
20 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
21 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
22 |
(** ML system and platform related **) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
23 |
|
26474 | 24 |
val forget_structure = PolyML.Compiler.forgetStructure; |
25 |
||
33213
1b550123f133
forget old some old option stuff from NJ -- superceded by material in Pure/General/basics.ML;
wenzelm
parents:
33060
diff
changeset
|
26 |
val _ = PolyML.Compiler.forgetValue "isSome"; |
1b550123f133
forget old some old option stuff from NJ -- superceded by material in Pure/General/basics.ML;
wenzelm
parents:
33060
diff
changeset
|
27 |
val _ = PolyML.Compiler.forgetValue "getOpt"; |
1b550123f133
forget old some old option stuff from NJ -- superceded by material in Pure/General/basics.ML;
wenzelm
parents:
33060
diff
changeset
|
28 |
val _ = PolyML.Compiler.forgetValue "valOf"; |
33004
715566791eb0
always qualify NJ's old List.foldl/foldr in Isabelle/ML;
wenzelm
parents:
32776
diff
changeset
|
29 |
val _ = PolyML.Compiler.forgetValue "foldl"; |
715566791eb0
always qualify NJ's old List.foldl/foldr in Isabelle/ML;
wenzelm
parents:
32776
diff
changeset
|
30 |
val _ = PolyML.Compiler.forgetValue "foldr"; |
31324
3ffa005c7701
removed print function from global ML name space, to reduce risk of surprises;
wenzelm
parents:
31319
diff
changeset
|
31 |
val _ = PolyML.Compiler.forgetValue "print"; |
32741
bf8881f6e343
hide "ref" by default, to enforce excplicit indication as Unsynchronized;
wenzelm
parents:
32737
diff
changeset
|
32 |
val _ = PolyML.Compiler.forgetValue "ref"; |
bf8881f6e343
hide "ref" by default, to enforce excplicit indication as Unsynchronized;
wenzelm
parents:
32737
diff
changeset
|
33 |
val _ = PolyML.Compiler.forgetType "ref"; |
31324
3ffa005c7701
removed print function from global ML name space, to reduce risk of surprises;
wenzelm
parents:
31319
diff
changeset
|
34 |
|
26474 | 35 |
|
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
36 |
(* Compiler options *) |
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 ml_system_fix_ints = false; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
39 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
40 |
PolyML.Compiler.printInAlphabeticalOrder := false; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
41 |
PolyML.Compiler.maxInlineSize := 80; |
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 |
(* old Poly/ML emulation *) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
45 |
|
31319
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
46 |
fun quit () = exit 0; |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
47 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
48 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
49 |
(* restore old-style character / string functions *) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
50 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
51 |
val ord = SML90.ord; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
52 |
val chr = SML90.chr; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
53 |
val explode = SML90.explode; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
54 |
val implode = SML90.implode; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
55 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
56 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
57 |
(* prompts *) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
58 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
59 |
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
|
60 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
61 |
|
36162
0bd034a80a9a
added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
wenzelm
parents:
35014
diff
changeset
|
62 |
(* toplevel printing *) |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
63 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
64 |
local |
32737
76fa673eee8b
Raw ML references as unsynchronized state variables.
wenzelm
parents:
31686
diff
changeset
|
65 |
val depth = Unsynchronized.ref 10; |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
66 |
in |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
67 |
fun get_print_depth () = ! depth; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
68 |
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
|
69 |
end; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
70 |
|
31319
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
71 |
val error_depth = PolyML.error_depth; |
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
72 |
|
36162
0bd034a80a9a
added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
wenzelm
parents:
35014
diff
changeset
|
73 |
val ml_make_string = "PolyML.makestring"; |
0bd034a80a9a
added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
wenzelm
parents:
35014
diff
changeset
|
74 |
|
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
75 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
76 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
77 |
(** interrupts **) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
78 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
79 |
local |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
80 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
81 |
val sig_int = 2; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
82 |
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
|
83 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
84 |
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
|
85 |
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
|
86 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
87 |
fun change_signal new_handler f x = |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
88 |
let |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
89 |
(*RACE wrt. other signals!*) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
90 |
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
|
91 |
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
|
92 |
val _ = Signal.signal (sig_int, old_handler); |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
93 |
in Exn.release result end; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
94 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
95 |
in |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
96 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
97 |
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
|
98 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
99 |
fun uninterruptible f = |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
100 |
change_signal Signal.SIG_IGN |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
101 |
(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
|
102 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
103 |
end; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
104 |
|
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 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
107 |
(** OS related **) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
108 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
109 |
(* current directory *) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
110 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
111 |
val cd = OS.FileSys.chDir; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
112 |
val pwd = OS.FileSys.getDir; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
113 |
|
28488
18fea7e88ea1
removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents:
28443
diff
changeset
|
114 |
fun process_id () = |
18fea7e88ea1
removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents:
28443
diff
changeset
|
115 |
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
|
116 |
|
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 |
(* getenv *) |
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 |
fun getenv var = |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
121 |
(case OS.Process.getEnv var of |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
122 |
NONE => "" |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
123 |
| SOME txt => txt); |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
124 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
125 |
|
31319
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
126 |
|
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
127 |
(** Runtime system **) |
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
128 |
|
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
129 |
val exception_trace = PolyML.exception_trace; |
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
130 |
val timing = PolyML.timing; |
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
131 |
val profiling = PolyML.profiling; |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
132 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
133 |
fun profile 0 f x = f x |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
134 |
| profile n f x = |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
135 |
let |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
136 |
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
|
137 |
val res = Exn.capture f x; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
138 |
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
|
139 |
in Exn.release res end; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
140 |