author  wenzelm 
Sun, 31 May 2009 14:51:21 +0200  
changeset 31312  1c00e4ff3c99 
parent 30672  beaadd5af500 
child 31321  fe786d4633b9 
permissions  rwrr 
4403  1 
(* Title: Pure/MLSystems/smlnj.ML 
2 

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

28443  6 
exception Interrupt; 
7 

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

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

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

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

12 
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

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

15 
use "MLSystems/ml_name_space.ML"; 
30619  16 
use "MLSystems/ml_pretty.ML"; 
30672
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30626
diff
changeset

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

18 

16542  19 

20 
(*lowlevel pointer equality*) 

16502  21 

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

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

23 
val pointer_eq = InlineT.ptreql; 
16528  24 

16502  25 

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

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

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

4403  32 

33 

34 
(* New Jersey ML parameters *) 

35 

36 
val _ = 

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

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

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

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

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

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

43 

44 
(* Poly/ML emulation *) 

45 

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

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

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

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

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

54 
fun print_depth n = 

55 
(depth := n; 

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

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

58 
end; 

4403  59 

26474  60 

5816  61 
(* compilerindependent timing functions *) 
4403  62 

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

63 
fun start_timing () = 
30187
b92b3375e919
end_timing: generalized result  message plus with explicit time values;
wenzelm
parents:
29564
diff
changeset

64 
let 
b92b3375e919
end_timing: generalized result  message plus with explicit time values;
wenzelm
parents:
29564
diff
changeset

65 
val timer = Timer.startCPUTimer (); 
b92b3375e919
end_timing: generalized result  message plus with explicit time values;
wenzelm
parents:
29564
diff
changeset

66 
val time = Timer.checkCPUTimer timer; 
b92b3375e919
end_timing: generalized result  message plus with explicit time values;
wenzelm
parents:
29564
diff
changeset

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

68 

30187
b92b3375e919
end_timing: generalized result  message plus with explicit time values;
wenzelm
parents:
29564
diff
changeset

69 
fun end_timing (timer, {sys, usr}) = 
b92b3375e919
end_timing: generalized result  message plus with explicit time values;
wenzelm
parents:
29564
diff
changeset

70 
let 
b92b3375e919
end_timing: generalized result  message plus with explicit time values;
wenzelm
parents:
29564
diff
changeset

71 
open Time; (*...for Time.toString, Time.+ and Time. *) 
b92b3375e919
end_timing: generalized result  message plus with explicit time values;
wenzelm
parents:
29564
diff
changeset

72 
val {sys = sys2, usr = usr2} = Timer.checkCPUTimer timer; 
b92b3375e919
end_timing: generalized result  message plus with explicit time values;
wenzelm
parents:
29564
diff
changeset

73 
val user = usr2  usr; 
b92b3375e919
end_timing: generalized result  message plus with explicit time values;
wenzelm
parents:
29564
diff
changeset

74 
val all = user + sys2  sys; 
b92b3375e919
end_timing: generalized result  message plus with explicit time values;
wenzelm
parents:
29564
diff
changeset

75 
val message = "User " ^ toString user ^ " All "^ toString all ^ " secs" handle Time => ""; 
b92b3375e919
end_timing: generalized result  message plus with explicit time values;
wenzelm
parents:
29564
diff
changeset

76 
in {message = message, user = user, all = all} end; 
21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

77 

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

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

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

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

81 
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

82 
in (sys, usr, gc) end; 
4403  83 

84 

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

87 
(Control.primaryPrompt := p1; Control.secondaryPrompt := p2); 
4977  88 

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

17511  92 
(*dummy implementation*) 
16681  93 
fun exception_trace f = f (); 
4977  94 

18384  95 
(*dummy implementation*) 
96 
fun print x = x; 

16681  97 

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

100 

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

101 

4403  102 
(* ML command execution *) 
103 

30672
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30626
diff
changeset

104 
fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt = 
5090  105 
let 
21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

106 
val ref out_orig = Control.Print.out; 
5090  107 

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

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

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

114 
Control.Print.out := out; 
30672
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30626
diff
changeset

115 
Backend.Interact.useStream (TextIO.openString (tune_source txt)) handle exn => 
22144  116 
(Control.Print.out := out_orig; 
30672
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30626
diff
changeset

117 
error ((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

118 
Control.Print.out := out_orig; 
10914  119 
if verbose then print (output ()) else () 
5090  120 
end; 
4403  121 

30672
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30626
diff
changeset

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

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

124 
val instream = TextIO.openIn name; 
26504  125 
val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); 
30672
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30626
diff
changeset

126 
in use_text context (1, name) verbose txt end; 
21770  127 

30672
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30626
diff
changeset

128 
fun forget_structure _ = (); 
26474  129 

21770  130 

30626  131 
(* toplevel pretty printing *) 
132 

133 
fun ml_pprint pps = 

134 
let 

135 
fun str "" = () 

136 
 str s = PrettyPrint.string pps s; 

137 
fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) = 

138 
(str bg; PrettyPrint.openHOVBox pps (PrettyPrint.Rel (dest_int ind)); 

139 
List.app pprint prts; PrettyPrint.closeBox pps; str en) 

140 
 pprint (ML_Pretty.String (s, _)) = str s 

141 
 pprint (ML_Pretty.Break (false, wd)) = PrettyPrint.break pps {nsp = dest_int wd, offset = 0} 

142 
 pprint (ML_Pretty.Break (true, _)) = PrettyPrint.newline pps; 

143 
in pprint end; 

144 

30672
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30626
diff
changeset

145 
fun toplevel_pp context path pp = 
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30626
diff
changeset

146 
use_text context (1, "pp") false 
30626  147 
("CompilerPPTable.install_pp [" ^ String.concatWith "," (map (fn s => "\"" ^ s ^ "\"") path) ^ 
148 
"] (fn pps => ml_pprint pps o Pretty.to_ML o (" ^ pp ^ "))"); 

149 

150 

4403  151 

5816  152 
(** interrupts **) 
153 

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

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

155 

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

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

158 
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

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

161 
in Exn.release result end; 
5816  162 

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

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

164 

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

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

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

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

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

174 
Exn.release (! result) 
12990  175 
end; 
5816  176 

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

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

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

179 
(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

180 

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

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

182 

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

183 

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

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

185 

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

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

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

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

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

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

191 
end; 
17511  192 

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

193 

5816  194 

4403  195 
(** OS related **) 
196 

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

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

198 

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

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

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

201 

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

202 

4403  203 
(* system command execution *) 
204 

26220  205 
val system_out = (fn (output, rc) => (output, mk_int rc)) o system_out; 
7855  206 

4403  207 

17824  208 
(*Convert a process ID to a decimal string (chiefly for tracing)*) 
28488
18fea7e88ea1
removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents:
28443
diff
changeset

209 
fun process_id pid = 
18fea7e88ea1
removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents:
28443
diff
changeset

210 
Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord (Posix.ProcEnv.getpid ()))); 
17824  211 

212 

4403  213 
(* getenv *) 
214 

215 
fun getenv var = 

216 
(case OS.Process.getEnv var of 

217 
NONE => "" 

218 
 SOME txt => txt); 