author  wenzelm 
Wed, 29 Dec 2010 12:37:15 +0100  
changeset 41411  3bcc3b9e1020 
parent 40748  591b6778d076 
child 42012  2c3fe3cbebae 
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; 
31427
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
31321
diff
changeset

7 
fun reraise exn = raise exn; 
28443  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"; 
34136  11 
use "General/exn.ML"; 
35014
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
35010
diff
changeset

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

14 
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

15 
use "MLSystems/multithreading.ML"; 
40393  16 
use "General/timing.ML"; 
28268
ac8431ecd57e
use_text/use_file now depend on explicit ML name space;
wenzelm
parents:
28151
diff
changeset

17 
use "MLSystems/ml_name_space.ML"; 
30619  18 
use "MLSystems/ml_pretty.ML"; 
38635
f76ad0771f67
added ML toplevel prettyprinting for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents:
36162
diff
changeset

19 
structure PolyML = struct end; 
f76ad0771f67
added ML toplevel prettyprinting for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents:
36162
diff
changeset

20 
use "MLSystems/pp_dummy.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

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

22 

16542  23 

24 
(*lowlevel pointer equality*) 

16502  25 

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

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

27 
val pointer_eq = InlineT.ptreql; 
16528  28 

41411  29 
fun share_common_data () = (); 
30 

16502  31 

4403  32 
(* restore oldstyle character / string functions *) 
33 

40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40393
diff
changeset

34 
val ord = mk_int o SML90.ord; 
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40393
diff
changeset

35 
val chr = SML90.chr o dest_int; 
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40393
diff
changeset

36 
val raw_explode = SML90.explode; 
10725  37 
val implode = SML90.implode; 
4403  38 

39 

40 
(* New Jersey ML parameters *) 

41 

42 
val _ = 

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

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

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

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

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

47 
Control.MC.matchRedundantError := false); 
4403  48 

49 

50 
(* Poly/ML emulation *) 

51 

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

52 
val exit = exit o dest_int; 
4403  53 
fun quit () = exit 0; 
54 

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

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

57 
val depth = ref (10: int); 
24329  58 
in 
59 
fun get_print_depth () = ! depth; 

60 
fun print_depth n = 

61 
(depth := n; 

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

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

64 
end; 

4403  65 

36162
0bd034a80a9a
added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
wenzelm
parents:
35014
diff
changeset

66 
val ml_make_string = "(fn _ => \"?\")"; 
0bd034a80a9a
added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
wenzelm
parents:
35014
diff
changeset

67 

26474  68 

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

71 
(Control.primaryPrompt := p1; Control.secondaryPrompt := p2); 
4977  72 

17511  73 
(*dummy implementation*) 
16681  74 
fun profile (n: int) f x = f x; 
75 

17511  76 
(*dummy implementation*) 
16681  77 
fun exception_trace f = f (); 
4977  78 

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

79 

4403  80 
(* ML command execution *) 
81 

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

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

84 
val ref out_orig = Control.Print.out; 
5090  85 

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

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

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

92 
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

93 
Backend.Interact.useStream (TextIO.openString (tune_source txt)) handle exn => 
22144  94 
(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

95 
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

96 
Control.Print.out := out_orig; 
10914  97 
if verbose then print (output ()) else () 
5090  98 
end; 
4403  99 

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

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

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

102 
val instream = TextIO.openIn name; 
26504  103 
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

104 
in use_text context (1, name) verbose txt end; 
21770  105 

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

106 
fun forget_structure _ = (); 
26474  107 

21770  108 

30626  109 
(* toplevel pretty printing *) 
110 

111 
fun ml_pprint pps = 

112 
let 

113 
fun str "" = () 

114 
 str s = PrettyPrint.string pps s; 

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

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

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

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

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

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

121 
in pprint end; 

122 

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

123 
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

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

127 

128 

4403  129 

5816  130 
(** interrupts **) 
131 

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

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

133 

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

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

136 
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

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

139 
in Exn.release result end; 
5816  140 

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

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

142 

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

143 
fun interruptible (f: 'a > 'b) x = 
12990  144 
let 
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn  hardly ever need to mention Interrupt literally;
wenzelm
parents:
38635
diff
changeset

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

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

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

152 
Exn.release (! result) 
12990  153 
end; 
5816  154 

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

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

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

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

158 

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

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

160 

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

161 

39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
39585
diff
changeset

162 
use "MLSystems/unsynchronized.ML"; 
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
39585
diff
changeset

163 

8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
39585
diff
changeset

164 

5816  165 

4403  166 
(** OS related **) 
167 

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

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

169 

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

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

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

172 

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

173 

4403  174 
(* getenv *) 
175 

176 
fun getenv var = 

177 
(case OS.Process.getEnv var of 

178 
NONE => "" 

179 
 SOME txt => txt); 