author | paulson |
Fri, 24 Nov 2000 11:07:38 +0100 | |
changeset 10517 | b9f7adf3ff11 |
parent 10209 | b24210573eca |
child 10518 | 20d4899f5d48 |
permissions | -rw-r--r-- |
9735 | 1 |
(* Title: Pure/ML-Systems/polyml.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1991 University of Cambridge |
|
5 |
||
9738 | 6 |
Compatibility file for Poly/ML (version 4.0). |
9735 | 7 |
*) |
8 |
||
9 |
(** ML system related **) |
|
10 |
||
9766 | 11 |
(* old Poly/ML emulation *) |
12 |
||
13 |
local |
|
14 |
val orig_exit = exit; |
|
15 |
in |
|
16 |
open PolyML; |
|
17 |
val exit = orig_exit; |
|
18 |
fun quit () = exit 0; |
|
19 |
end; |
|
9735 | 20 |
|
21 |
||
22 |
(* restore old-style character / string functions *) |
|
23 |
||
24 |
fun ord s = Char.ord (String.sub (s, 0)); |
|
25 |
val chr = str o Char.chr; |
|
26 |
val explode = (map str) o String.explode; |
|
27 |
val implode = String.concat; |
|
28 |
||
29 |
||
30 |
(*Note start point for timing*) |
|
31 |
fun startTiming() = |
|
32 |
let val CPUtimer = Timer.startCPUTimer(); |
|
33 |
val time = Timer.checkCPUTimer(CPUtimer) |
|
34 |
in (CPUtimer,time) end; |
|
35 |
||
36 |
(*Finish timing and return string*) |
|
37 |
fun endTiming (CPUtimer, {sys,usr}) = |
|
38 |
let open Time (*...for Time.toString, Time.+ and Time.- *) |
|
39 |
val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer) |
|
40 |
in "User " ^ toString (usr2-usr) ^ |
|
41 |
" All "^ toString (sys2-sys + usr2-usr) ^ |
|
42 |
" secs" |
|
43 |
handle Time => "" |
|
44 |
end; |
|
45 |
||
46 |
||
47 |
(* prompts *) |
|
48 |
||
49 |
fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2); |
|
50 |
||
51 |
||
52 |
(* toplevel pretty printing (see also Pure/install_pp.ML) *) |
|
53 |
||
9766 | 54 |
fun make_pp _ pprint (str, blk, brk, en) _ _ obj = |
9735 | 55 |
pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0), |
56 |
fn () => brk (99999, 0), en); |
|
57 |
||
58 |
||
59 |
(* ML command execution -- 'eval' *) |
|
60 |
||
61 |
local |
|
62 |
||
63 |
fun drop_last [] = [] |
|
64 |
| drop_last [x] = [] |
|
65 |
| drop_last (x :: xs) = x :: drop_last xs; |
|
66 |
||
67 |
val drop_last_char = implode o drop_last o explode; |
|
68 |
||
69 |
in |
|
70 |
||
71 |
fun use_text print verbose txt = |
|
72 |
let |
|
73 |
val in_buffer = ref (explode txt); |
|
74 |
val out_buffer = ref ([]: string list); |
|
75 |
||
76 |
fun get () = |
|
77 |
(case ! in_buffer of |
|
78 |
[] => "" |
|
79 |
| c :: cs => (in_buffer := cs; c)); |
|
80 |
fun put s = out_buffer := s :: ! out_buffer; |
|
81 |
||
82 |
fun exec () = |
|
83 |
(case ! in_buffer of |
|
84 |
[] => () |
|
85 |
| _ => (PolyML.compiler (get, put) (); exec ())); |
|
86 |
||
87 |
fun show_output () = print (drop_last_char (implode (rev (! out_buffer)))); |
|
88 |
in |
|
89 |
exec () handle exn => (show_output (); raise exn); |
|
90 |
if verbose then show_output () else () |
|
91 |
end; |
|
92 |
||
93 |
end; |
|
94 |
||
95 |
||
96 |
||
9766 | 97 |
(** interrupts **) |
98 |
||
10517
b9f7adf3ff11
added exception Interrupt for use in function Library/try
paulson
parents:
10209
diff
changeset
|
99 |
exception Interrupt; |
b9f7adf3ff11
added exception Interrupt for use in function Library/try
paulson
parents:
10209
diff
changeset
|
100 |
|
9766 | 101 |
local |
102 |
||
103 |
datatype 'a result = |
|
104 |
Result of 'a | |
|
105 |
Exn of exn; |
|
106 |
||
107 |
fun capture f x = Result (f x) handle exn => Exn exn; |
|
108 |
||
109 |
fun release (Result x) = x |
|
110 |
| release (Exn exn) = raise exn; |
|
111 |
||
9735 | 112 |
|
9766 | 113 |
val sig_int = 2; |
114 |
||
115 |
fun change_signal new_handler f x = |
|
116 |
let |
|
117 |
(*RACE wrt. other signals*) |
|
118 |
val old_handler = Signal.signal (sig_int, new_handler); |
|
119 |
val result = capture f x; |
|
120 |
val _ = Signal.signal (sig_int, old_handler); |
|
121 |
in release result end; |
|
122 |
||
10209
b24210573eca
install default_handler for SIGINT initially as well;
wenzelm
parents:
10194
diff
changeset
|
123 |
val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ()); |
b24210573eca
install default_handler for SIGINT initially as well;
wenzelm
parents:
10194
diff
changeset
|
124 |
|
9766 | 125 |
in |
126 |
||
10209
b24210573eca
install default_handler for SIGINT initially as well;
wenzelm
parents:
10194
diff
changeset
|
127 |
val _ = Signal.signal (sig_int, default_handler); |
b24210573eca
install default_handler for SIGINT initially as well;
wenzelm
parents:
10194
diff
changeset
|
128 |
|
9766 | 129 |
fun mask_interrupt f = change_signal Signal.SIG_IGN f; |
10209
b24210573eca
install default_handler for SIGINT initially as well;
wenzelm
parents:
10194
diff
changeset
|
130 |
fun exhibit_interrupt f = change_signal default_handler f; |
9766 | 131 |
|
132 |
end; |
|
9735 | 133 |
|
134 |
||
135 |
||
136 |
(** OS related **) |
|
137 |
||
138 |
(* system command execution *) |
|
139 |
||
140 |
(*execute Unix command which doesn't take any input from stdin and |
|
141 |
sends its output to stdout; could be done more easily by Unix.execute, |
|
142 |
but that function doesn't use the PATH*) |
|
143 |
fun execute command = |
|
144 |
let |
|
145 |
val tmp_name = OS.FileSys.tmpName (); |
|
146 |
val is = (OS.Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name); |
|
147 |
val result = TextIO.inputAll is; |
|
148 |
in |
|
149 |
TextIO.closeIn is; |
|
150 |
OS.FileSys.remove tmp_name; |
|
151 |
result |
|
152 |
end; |
|
153 |
||
154 |
(*plain version; with return code*) |
|
155 |
fun system cmd = |
|
156 |
if OS.Process.isSuccess (OS.Process.system cmd) then 0 else 1; |
|
157 |
||
158 |
||
159 |
(* file handling *) |
|
160 |
||
161 |
(*get time of last modification*) |
|
162 |
fun file_info name = Time.toString (OS.FileSys.modTime name) handle _ => ""; |
|
163 |
||
164 |
||
165 |
(* getenv *) |
|
166 |
||
167 |
fun getenv var = |
|
168 |
(case OS.Process.getEnv var of |
|
169 |
NONE => "" |
|
170 |
| SOME txt => txt); |
|
171 |
||
172 |
||
173 |
(* non-ASCII input (see also Thy/use.ML) *) |
|
174 |
||
175 |
val needs_filtered_use = true; |