author  wenzelm 
Wed, 01 Oct 2008 12:00:02 +0200  
changeset 28443  de653f1ad78b 
parent 28284  2161665a0a5d 
child 28488  18fea7e88ea1 
permissions  rwrr 
4403  1 
(* Title: Pure/MLSystems/smlnj.ML 
2 
ID: $Id$ 

3 

5708  4 
Compatibility file for Standard ML of New Jersey 110 or later. 
4403  5 
*) 
6 

28443  7 
exception Interrupt; 
8 

24599
7b0ecf9a9055
use_text/file: tune text (cf. ML_Parse.fix_ints);
wenzelm
parents:
24329
diff
changeset

9 
use "MLSystems/proper_int.ML"; 
7b0ecf9a9055
use_text/file: tune text (cf. ML_Parse.fix_ints);
wenzelm
parents:
24329
diff
changeset

10 
use "MLSystems/overloading_smlnj.ML"; 
23965
f93e509659c1
MLSystems/exn.ML, MLSystems/multithreading_dummy.ML;
wenzelm
parents:
23921
diff
changeset

11 
use "MLSystems/exn.ML"; 
25732  12 
use "MLSystems/universal.ML"; 
28151
61f9c918b410
explicit use of universal.ML and dummy_thread.ML;
wenzelm
parents:
26885
diff
changeset

13 
use "MLSystems/thread_dummy.ML"; 
24688
a5754ca5c510
replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
24599
diff
changeset

14 
use "MLSystems/multithreading.ML"; 
26220  15 
use "MLSystems/system_shell.ML"; 
28268
ac8431ecd57e
use_text/use_file now depend on explicit ML name space;
wenzelm
parents:
28151
diff
changeset

16 
use "MLSystems/ml_name_space.ML"; 
23921
947152add153
added compatibility file for ML systems without multithreading;
wenzelm
parents:
23826
diff
changeset

17 

16542  18 

19 
(*lowlevel pointer equality*) 

16502  20 

21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

21 
CM.autoload "$smlnj/init/init.cmi"; 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

22 
val pointer_eq = InlineT.ptreql; 
16528  23 

16502  24 

4403  25 
(* restore oldstyle character / string functions *) 
26 

24145  27 
val ord = mk_int o SML90.ord; 
28 
val chr = SML90.chr o dest_int; 

10725  29 
val explode = SML90.explode; 
30 
val implode = SML90.implode; 

4403  31 

32 

33 
(* New Jersey ML parameters *) 

34 

35 
val _ = 

21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

36 
(Control.Print.printLength := 1000; 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

37 
Control.Print.printDepth := 350; 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

38 
Control.Print.stringDepth := 250; 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

39 
Control.Print.signatures := 2; 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

40 
Control.MC.matchRedundantError := false); 
4403  41 

42 

43 
(* Poly/ML emulation *) 

44 

24599
7b0ecf9a9055
use_text/file: tune text (cf. ML_Parse.fix_ints);
wenzelm
parents:
24329
diff
changeset

45 
val exit = exit o dest_int; 
4403  46 
fun quit () = exit 0; 
47 

48 
(*limit the printing depth  divided by 2 for comparibility with Poly/ML*) 

24329  49 
local 
24599
7b0ecf9a9055
use_text/file: tune text (cf. ML_Parse.fix_ints);
wenzelm
parents:
24329
diff
changeset

50 
val depth = ref (10: int); 
24329  51 
in 
52 
fun get_print_depth () = ! depth; 

53 
fun print_depth n = 

54 
(depth := n; 

55 
Control.Print.printDepth := dest_int n div 2; 

56 
Control.Print.printLength := dest_int n); 

57 
end; 

4403  58 

26474  59 

5816  60 
(* compilerindependent timing functions *) 
4403  61 

21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

62 
fun start_timing () = 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

63 
let val CPUtimer = Timer.startCPUTimer(); 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

64 
val time = Timer.checkCPUTimer(CPUtimer) 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

65 
in (CPUtimer,time) end; 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

66 

6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

67 
fun end_timing (CPUtimer, {sys,usr}) = 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

68 
let open Time (*...for Time.toString, Time.+ and Time. *) 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

69 
val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer) 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

70 
in "User " ^ toString (usr2usr) ^ 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

71 
" All "^ toString (sys2sys + usr2usr) ^ 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

72 
" secs" 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

73 
handle Time => "" 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

74 
end; 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

75 

6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

76 
fun check_timer timer = 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

77 
let 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

78 
val {sys, usr} = Timer.checkCPUTimer timer; 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

79 
val gc = Timer.checkGCTime timer; (* FIXME already included in usr? *) 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

80 
in (sys, usr, gc) end; 
4403  81 

82 

16660  83 
(*prompts*) 
4977  84 
fun ml_prompts p1 p2 = 
21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

85 
(Control.primaryPrompt := p1; Control.secondaryPrompt := p2); 
4977  86 

17511  87 
(*dummy implementation*) 
16681  88 
fun profile (n: int) f x = f x; 
89 

17511  90 
(*dummy implementation*) 
16681  91 
fun exception_trace f = f (); 
4977  92 

18384  93 
(*dummy implementation*) 
94 
fun print x = x; 

16681  95 

23770  96 
(*dummy implementation*) 
97 
fun makestring x = "dummy string for SML New Jersey"; 

98 

21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

99 

24290  100 
(* toplevel pretty printing (see also Pure/pure_setup.ML) *) 
4403  101 

21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

102 
fun make_pp path pprint = 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

103 
let 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

104 
open PrettyPrint; 
4403  105 

21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

106 
fun pp pps obj = 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

107 
pprint obj 
24145  108 
(string pps, openHOVBox pps o Rel o dest_int, 
109 
fn wd => break pps {nsp=dest_int wd, offset=0}, fn () => newline pps, 

21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

110 
fn () => closeBox pps); 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

111 
in (path, pp) end; 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

112 

6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

113 
fun install_pp (path, pp) = CompilerPPTable.install_pp path pp; 
4403  114 

115 

116 
(* ML command execution *) 

117 

28268
ac8431ecd57e
use_text/use_file now depend on explicit ML name space;
wenzelm
parents:
28151
diff
changeset

118 
fun use_text (tune: string > string) _ _ (line: int, name) (print, err) verbose txt = 
5090  119 
let 
21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

120 
val ref out_orig = Control.Print.out; 
5090  121 

122 
val out_buffer = ref ([]: string list); 

123 
val out = {say = (fn s => out_buffer := s :: ! out_buffer), flush = (fn () => ())}; 

10914  124 
fun output () = 
7890  125 
let val str = implode (rev (! out_buffer)) 
10914  126 
in String.substring (str, 0, Int.max (0, size str  1)) end; 
5090  127 
in 
21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

128 
Control.Print.out := out; 
24599
7b0ecf9a9055
use_text/file: tune text (cf. ML_Parse.fix_ints);
wenzelm
parents:
24329
diff
changeset

129 
Backend.Interact.useStream (TextIO.openString (tune txt)) handle exn => 
22144  130 
(Control.Print.out := out_orig; 
131 
err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn); 

21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

132 
Control.Print.out := out_orig; 
10914  133 
if verbose then print (output ()) else () 
5090  134 
end; 
4403  135 

28268
ac8431ecd57e
use_text/use_file now depend on explicit ML name space;
wenzelm
parents:
28151
diff
changeset

136 
fun use_file tune str_of_pos name_space output verbose name = 
24599
7b0ecf9a9055
use_text/file: tune text (cf. ML_Parse.fix_ints);
wenzelm
parents:
24329
diff
changeset

137 
let 
7b0ecf9a9055
use_text/file: tune text (cf. ML_Parse.fix_ints);
wenzelm
parents:
24329
diff
changeset

138 
val instream = TextIO.openIn name; 
26504  139 
val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); 
28268
ac8431ecd57e
use_text/use_file now depend on explicit ML name space;
wenzelm
parents:
28151
diff
changeset

140 
in use_text tune str_of_pos name_space (1, name) output verbose txt end; 
21770  141 

26474  142 
fun forget_structure name = 
28284
2161665a0a5d
use_text/use_file now depend on explicit ML name space;
wenzelm
parents:
28268
diff
changeset

143 
use_text (fn x => x) (fn _ => "") () (1, "ML") (TextIO.print, fn s => raise Fail s) false 
26474  144 
("structure " ^ name ^ " = struct end"); 
145 

21770  146 

4403  147 

5816  148 
(** interrupts **) 
149 

26084
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

150 
local 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

151 

a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

152 
fun change_signal new_handler f x = 
5816  153 
let 
26084
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

154 
val old_handler = Signals.setHandler (Signals.sigINT, new_handler); 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

155 
val result = Exn.capture (f old_handler) x; 
12990  156 
val _ = Signals.setHandler (Signals.sigINT, old_handler); 
23965
f93e509659c1
MLSystems/exn.ML, MLSystems/multithreading_dummy.ML;
wenzelm
parents:
23921
diff
changeset

157 
in Exn.release result end; 
5816  158 

26084
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

159 
in 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

160 

a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

161 
fun interruptible (f: 'a > 'b) x = 
12990  162 
let 
26084
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

163 
val result = ref (Exn.Exn Interrupt: 'b Exn.result); 
12990  164 
val old_handler = Signals.inqHandler Signals.sigINT; 
5816  165 
in 
12990  166 
SMLofNJ.Cont.callcc (fn cont => 
26084
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

167 
(Signals.setHandler (Signals.sigINT, Signals.HANDLER (fn _ => cont)); 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

168 
result := Exn.capture f x)); 
12990  169 
Signals.setHandler (Signals.sigINT, old_handler); 
26084
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

170 
Exn.release (! result) 
12990  171 
end; 
5816  172 

26084
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

173 
fun uninterruptible f = 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

174 
change_signal Signals.IGNORE 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

175 
(fn old_handler => f (fn g => change_signal old_handler (fn _ => g))); 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

176 

a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

177 
end; 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

178 

21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

179 

6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

180 
(* basis library fixes *) 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

181 

6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

182 
structure TextIO = 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

183 
struct 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

184 
open TextIO; 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
22144
diff
changeset

185 
fun inputLine is = TextIO.inputLine is 
21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

186 
handle IO.Io _ => raise Interrupt; 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

187 
end; 
17511  188 

18790
418131f631fc
interrupt_timeout now raises Interrupt instead of SML90.Interrupt
webertj
parents:
18760
diff
changeset

189 

16542  190 
(** Signal handling: emulation of the Poly/ML Signal structure. Note that types 
15702
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

191 
Posix.Signal.signal and Signals.signal differ **) 
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

192 

2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

193 
structure IsaSignal = 
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

194 
struct 
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

195 

2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

196 
datatype sig_handle = SIG_DFL  SIG_IGN  SIG_HANDLE of Signals.signal > unit; 
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

197 

16542  198 
(*From the SML/NJ documentation: "HANDLER(f) installs a handler for a 
199 
signal. When signal is delivered to the process, the execution state 

200 
of the current thread will be bundled up as a continuation k, then 

201 
f(signal,n,k) will be called. The number n is the number of times 

202 
signal has been signalled since the last time f was invoked for it."*) 

15702
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

203 

2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

204 
fun toAction SIG_DFL = Signals.DEFAULT 
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

205 
 toAction SIG_IGN = Signals.IGNORE 
16542  206 
 toAction (SIG_HANDLE iu) = 
15702
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

207 
Signals.HANDLER (fn (signo,_,cont) => (iu signo; cont)); 
16542  208 

15702
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

209 
(*The types are correct, but I'm not sure about the semantics!*) 
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

210 
fun fromAction Signals.DEFAULT = SIG_DFL 
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

211 
 fromAction Signals.IGNORE = SIG_IGN 
16542  212 
 fromAction (Signals.HANDLER f) = 
15702
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

213 
SIG_HANDLE (fn signo => SMLofNJ.Cont.callcc (fn k => (f (signo,0,k); ()))); 
16542  214 

15702
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

215 
(*Poly/ML version has type int * sig_handle > sig_handle*) 
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

216 
fun signal (signo, sh) = fromAction (Signals.setHandler (signo, toAction sh)); 
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

217 

2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

218 
val usr1 = UnixSignals.sigUSR1 
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

219 
val usr2 = UnixSignals.sigUSR2 
17763  220 
val alrm = UnixSignals.sigALRM 
221 
val chld = UnixSignals.sigCHLD 

222 
val cont = UnixSignals.sigCONT 

223 
val int = UnixSignals.sigINT 

224 
val quit = UnixSignals.sigQUIT 

225 
val term = UnixSignals.sigTERM 

15702
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

226 

2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

227 
end; 
5816  228 

229 

4403  230 
(** OS related **) 
231 

23826
463903573934
moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents:
23770
diff
changeset

232 
(* current directory *) 
463903573934
moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents:
23770
diff
changeset

233 

463903573934
moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents:
23770
diff
changeset

234 
val cd = OS.FileSys.chDir; 
463903573934
moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents:
23770
diff
changeset

235 
val pwd = OS.FileSys.getDir; 
463903573934
moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents:
23770
diff
changeset

236 

463903573934
moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents:
23770
diff
changeset

237 

4403  238 
(* system command execution *) 
239 

26220  240 
val system_out = (fn (output, rc) => (output, mk_int rc)) o system_out; 
7855  241 

4403  242 

17824  243 
(*Convert a process ID to a decimal string (chiefly for tracing)*) 
21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

244 
fun string_of_pid pid = 
26220  245 
Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord pid)); 
17824  246 

247 

4403  248 
(* getenv *) 
249 

250 
fun getenv var = 

251 
(case OS.Process.getEnv var of 

252 
NONE => "" 

253 
 SOME txt => txt); 