author | wenzelm |
Sat, 06 Feb 2010 22:01:48 +0100 | |
changeset 35014 | a725ff6ead26 |
parent 35010 | d6e492cea6e4 |
child 36162 | 0bd034a80a9a |
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"; |
35014
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
35010
diff
changeset
|
9 |
use "ML-Systems/single_assignment_polyml.ML"; |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
10 |
use "ML-Systems/multithreading.ML"; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
11 |
use "ML-Systems/time_limit.ML"; |
31686
e54ae15335a1
more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
31324
diff
changeset
|
12 |
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
|
13 |
use "ML-Systems/bash.ML"; |
30619 | 14 |
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
|
15 |
use "ML-Systems/use_context.ML"; |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
16 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
17 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
18 |
(** ML system and platform related **) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
19 |
|
26474 | 20 |
val forget_structure = PolyML.Compiler.forgetStructure; |
21 |
||
33213
1b550123f133
forget old some old option stuff from NJ -- superceded by material in Pure/General/basics.ML;
wenzelm
parents:
33060
diff
changeset
|
22 |
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
|
23 |
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
|
24 |
val _ = PolyML.Compiler.forgetValue "valOf"; |
33004
715566791eb0
always qualify NJ's old List.foldl/foldr in Isabelle/ML;
wenzelm
parents:
32776
diff
changeset
|
25 |
val _ = PolyML.Compiler.forgetValue "foldl"; |
715566791eb0
always qualify NJ's old List.foldl/foldr in Isabelle/ML;
wenzelm
parents:
32776
diff
changeset
|
26 |
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
|
27 |
val _ = PolyML.Compiler.forgetValue "print"; |
32741
bf8881f6e343
hide "ref" by default, to enforce excplicit indication as Unsynchronized;
wenzelm
parents:
32737
diff
changeset
|
28 |
val _ = PolyML.Compiler.forgetValue "ref"; |
bf8881f6e343
hide "ref" by default, to enforce excplicit indication as Unsynchronized;
wenzelm
parents:
32737
diff
changeset
|
29 |
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
|
30 |
|
26474 | 31 |
|
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
32 |
(* Compiler options *) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
33 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
34 |
val ml_system_fix_ints = false; |
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 |
PolyML.Compiler.printInAlphabeticalOrder := false; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
37 |
PolyML.Compiler.maxInlineSize := 80; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
38 |
|
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 |
(* old Poly/ML emulation *) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
41 |
|
31319
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
42 |
fun quit () = exit 0; |
26215
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 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
45 |
(* restore old-style character / string functions *) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
46 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
47 |
val ord = SML90.ord; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
48 |
val chr = SML90.chr; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
49 |
val explode = SML90.explode; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
50 |
val implode = SML90.implode; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
51 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
52 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
53 |
(* prompts *) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
54 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
55 |
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
|
56 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
57 |
|
30625
d53d1a16d5ee
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents:
30619
diff
changeset
|
58 |
(* print depth *) |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
59 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
60 |
local |
32737
76fa673eee8b
Raw ML references as unsynchronized state variables.
wenzelm
parents:
31686
diff
changeset
|
61 |
val depth = Unsynchronized.ref 10; |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
62 |
in |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
63 |
fun get_print_depth () = ! depth; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
64 |
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
|
65 |
end; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
66 |
|
31319
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
67 |
val error_depth = PolyML.error_depth; |
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
68 |
|
26215
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 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
71 |
(** interrupts **) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
72 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
73 |
local |
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 |
val sig_int = 2; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
76 |
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
|
77 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
78 |
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
|
79 |
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
|
80 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
81 |
fun change_signal new_handler f x = |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
82 |
let |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
83 |
(*RACE wrt. other signals!*) |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
84 |
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
|
85 |
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
|
86 |
val _ = Signal.signal (sig_int, old_handler); |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
87 |
in Exn.release result end; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
88 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
89 |
in |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
90 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
91 |
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
|
92 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
93 |
fun uninterruptible f = |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
94 |
change_signal Signal.SIG_IGN |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
95 |
(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
|
96 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
97 |
end; |
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 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
100 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
101 |
(** OS related **) |
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 |
(* current directory *) |
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 |
val cd = OS.FileSys.chDir; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
106 |
val pwd = OS.FileSys.getDir; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
107 |
|
28488
18fea7e88ea1
removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents:
28443
diff
changeset
|
108 |
fun process_id () = |
18fea7e88ea1
removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents:
28443
diff
changeset
|
109 |
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
|
110 |
|
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 |
(* getenv *) |
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 |
fun getenv var = |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
115 |
(case OS.Process.getEnv var of |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
116 |
NONE => "" |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
117 |
| SOME txt => txt); |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
118 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
119 |
|
31319
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
120 |
|
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
121 |
(** Runtime system **) |
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
122 |
|
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
123 |
val exception_trace = PolyML.exception_trace; |
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
124 |
val timing = PolyML.timing; |
6974449ddea9
no longer open PolyML -- to avoid surprises within the global name space;
wenzelm
parents:
31308
diff
changeset
|
125 |
val profiling = PolyML.profiling; |
26215
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 |
fun profile 0 f x = f x |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
128 |
| profile n f x = |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
129 |
let |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
130 |
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
|
131 |
val res = Exn.capture f x; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
132 |
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
|
133 |
in Exn.release res end; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff
changeset
|
134 |