wenzelm@26215
|
1 |
(* Title: Pure/ML-Systems/polyml_common.ML
|
wenzelm@26215
|
2 |
|
wenzelm@26215
|
3 |
Compatibility file for Poly/ML -- common part for 4.x and 5.x.
|
wenzelm@26215
|
4 |
*)
|
wenzelm@26215
|
5 |
|
wenzelm@28443
|
6 |
exception Interrupt = SML90.Interrupt;
|
wenzelm@28443
|
7 |
|
wenzelm@26215
|
8 |
use "ML-Systems/exn.ML";
|
wenzelm@26215
|
9 |
use "ML-Systems/multithreading.ML";
|
wenzelm@26215
|
10 |
use "ML-Systems/time_limit.ML";
|
wenzelm@26220
|
11 |
use "ML-Systems/system_shell.ML";
|
wenzelm@28268
|
12 |
use "ML-Systems/ml_name_space.ML";
|
wenzelm@30622
|
13 |
use "ML-Systems/ml_pretty.ML";
|
wenzelm@26215
|
14 |
|
wenzelm@26215
|
15 |
|
wenzelm@26215
|
16 |
(** ML system and platform related **)
|
wenzelm@26215
|
17 |
|
wenzelm@26474
|
18 |
val forget_structure = PolyML.Compiler.forgetStructure;
|
wenzelm@26474
|
19 |
|
wenzelm@26474
|
20 |
|
wenzelm@26215
|
21 |
(* Compiler options *)
|
wenzelm@26215
|
22 |
|
wenzelm@26215
|
23 |
val ml_system_fix_ints = false;
|
wenzelm@26215
|
24 |
|
wenzelm@26215
|
25 |
PolyML.Compiler.printInAlphabeticalOrder := false;
|
wenzelm@26215
|
26 |
PolyML.Compiler.maxInlineSize := 80;
|
wenzelm@26215
|
27 |
|
wenzelm@26215
|
28 |
|
wenzelm@26215
|
29 |
(* old Poly/ML emulation *)
|
wenzelm@26215
|
30 |
|
wenzelm@26215
|
31 |
local
|
wenzelm@26215
|
32 |
val orig_exit = exit;
|
wenzelm@26215
|
33 |
in
|
wenzelm@26215
|
34 |
open PolyML;
|
wenzelm@26215
|
35 |
val exit = orig_exit;
|
wenzelm@26215
|
36 |
fun quit () = exit 0;
|
wenzelm@26215
|
37 |
end;
|
wenzelm@26215
|
38 |
|
wenzelm@26215
|
39 |
|
wenzelm@26215
|
40 |
(* restore old-style character / string functions *)
|
wenzelm@26215
|
41 |
|
wenzelm@26215
|
42 |
val ord = SML90.ord;
|
wenzelm@26215
|
43 |
val chr = SML90.chr;
|
wenzelm@26215
|
44 |
val explode = SML90.explode;
|
wenzelm@26215
|
45 |
val implode = SML90.implode;
|
wenzelm@26215
|
46 |
|
wenzelm@26215
|
47 |
|
wenzelm@26215
|
48 |
(* compiler-independent timing functions *)
|
wenzelm@26215
|
49 |
|
wenzelm@26215
|
50 |
fun start_timing () =
|
wenzelm@30187
|
51 |
let
|
wenzelm@30187
|
52 |
val timer = Timer.startCPUTimer ();
|
wenzelm@30187
|
53 |
val time = Timer.checkCPUTimer timer;
|
wenzelm@30187
|
54 |
in (timer, time) end;
|
wenzelm@26215
|
55 |
|
wenzelm@30187
|
56 |
fun end_timing (timer, {sys, usr}) =
|
wenzelm@30187
|
57 |
let
|
wenzelm@30187
|
58 |
open Time; (*...for Time.toString, Time.+ and Time.- *)
|
wenzelm@30187
|
59 |
val {sys = sys2, usr = usr2} = Timer.checkCPUTimer timer;
|
wenzelm@30187
|
60 |
val user = usr2 - usr;
|
wenzelm@30187
|
61 |
val all = user + sys2 - sys;
|
wenzelm@30187
|
62 |
val message = "User " ^ toString user ^ " All "^ toString all ^ " secs" handle Time => "";
|
wenzelm@30187
|
63 |
in {message = message, user = user, all = all} end;
|
wenzelm@26215
|
64 |
|
wenzelm@26215
|
65 |
fun check_timer timer =
|
wenzelm@26215
|
66 |
let
|
wenzelm@26215
|
67 |
val {sys, usr} = Timer.checkCPUTimer timer;
|
wenzelm@26215
|
68 |
val gc = Timer.checkGCTime timer; (* FIXME already included in usr? *)
|
wenzelm@26215
|
69 |
in (sys, usr, gc) end;
|
wenzelm@26215
|
70 |
|
wenzelm@26215
|
71 |
|
wenzelm@26215
|
72 |
(* prompts *)
|
wenzelm@26215
|
73 |
|
wenzelm@26215
|
74 |
fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
|
wenzelm@26215
|
75 |
|
wenzelm@26215
|
76 |
|
wenzelm@26215
|
77 |
(* toplevel pretty printing (see also Pure/pure_setup.ML) *)
|
wenzelm@26215
|
78 |
|
wenzelm@26215
|
79 |
fun make_pp _ pprint (str, blk, brk, en) _ _ obj =
|
wenzelm@26215
|
80 |
pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
|
wenzelm@26215
|
81 |
fn () => brk (99999, 0), en);
|
wenzelm@26215
|
82 |
|
wenzelm@26215
|
83 |
(*print depth*)
|
wenzelm@26215
|
84 |
local
|
wenzelm@26215
|
85 |
val depth = ref 10;
|
wenzelm@26215
|
86 |
in
|
wenzelm@26215
|
87 |
fun get_print_depth () = ! depth;
|
wenzelm@26215
|
88 |
fun print_depth n = (depth := n; PolyML.print_depth n);
|
wenzelm@26215
|
89 |
end;
|
wenzelm@26215
|
90 |
|
wenzelm@26215
|
91 |
|
wenzelm@26215
|
92 |
|
wenzelm@26215
|
93 |
(** interrupts **)
|
wenzelm@26215
|
94 |
|
wenzelm@26215
|
95 |
local
|
wenzelm@26215
|
96 |
|
wenzelm@26215
|
97 |
val sig_int = 2;
|
wenzelm@26215
|
98 |
val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ());
|
wenzelm@26215
|
99 |
|
wenzelm@26215
|
100 |
val _ = Signal.signal (sig_int, default_handler);
|
wenzelm@26380
|
101 |
val _ = PolyML.onEntry (fn () => (Signal.signal (sig_int, default_handler); ()));
|
wenzelm@26215
|
102 |
|
wenzelm@26215
|
103 |
fun change_signal new_handler f x =
|
wenzelm@26215
|
104 |
let
|
wenzelm@26215
|
105 |
(*RACE wrt. other signals!*)
|
wenzelm@26215
|
106 |
val old_handler = Signal.signal (sig_int, new_handler);
|
wenzelm@26215
|
107 |
val result = Exn.capture (f old_handler) x;
|
wenzelm@26215
|
108 |
val _ = Signal.signal (sig_int, old_handler);
|
wenzelm@26215
|
109 |
in Exn.release result end;
|
wenzelm@26215
|
110 |
|
wenzelm@26215
|
111 |
in
|
wenzelm@26215
|
112 |
|
wenzelm@26215
|
113 |
fun interruptible f = change_signal default_handler (fn _ => f);
|
wenzelm@26215
|
114 |
|
wenzelm@26215
|
115 |
fun uninterruptible f =
|
wenzelm@26215
|
116 |
change_signal Signal.SIG_IGN
|
wenzelm@26215
|
117 |
(fn old_handler => f (fn g => change_signal old_handler (fn _ => g)));
|
wenzelm@26215
|
118 |
|
wenzelm@26215
|
119 |
end;
|
wenzelm@26215
|
120 |
|
wenzelm@26215
|
121 |
|
wenzelm@26215
|
122 |
|
wenzelm@26215
|
123 |
(** OS related **)
|
wenzelm@26215
|
124 |
|
wenzelm@26215
|
125 |
(* current directory *)
|
wenzelm@26215
|
126 |
|
wenzelm@26215
|
127 |
val cd = OS.FileSys.chDir;
|
wenzelm@26215
|
128 |
val pwd = OS.FileSys.getDir;
|
wenzelm@26215
|
129 |
|
wenzelm@28488
|
130 |
fun process_id () =
|
wenzelm@28488
|
131 |
Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord (Posix.ProcEnv.getpid ())));
|
wenzelm@26215
|
132 |
|
wenzelm@26215
|
133 |
|
wenzelm@26215
|
134 |
(* getenv *)
|
wenzelm@26215
|
135 |
|
wenzelm@26215
|
136 |
fun getenv var =
|
wenzelm@26215
|
137 |
(case OS.Process.getEnv var of
|
wenzelm@26215
|
138 |
NONE => ""
|
wenzelm@26215
|
139 |
| SOME txt => txt);
|
wenzelm@26215
|
140 |
|
wenzelm@26215
|
141 |
|
wenzelm@26215
|
142 |
(* profile execution *)
|
wenzelm@26215
|
143 |
|
wenzelm@26215
|
144 |
fun profile 0 f x = f x
|
wenzelm@26215
|
145 |
| profile n f x =
|
wenzelm@26215
|
146 |
let
|
wenzelm@26215
|
147 |
val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
|
wenzelm@26215
|
148 |
val res = Exn.capture f x;
|
wenzelm@26215
|
149 |
val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
|
wenzelm@26215
|
150 |
in Exn.release res end;
|
wenzelm@26215
|
151 |
|