author  wenzelm 
Sun, 31 May 2009 15:03:34 +0200  
changeset 31313  97800f7e80b4 
parent 31312  1c00e4ff3c99 
child 31427  5a07cc86675d 
permissions  rwrr 
21653  1 
(* Title: Pure/MLSystems/polyml5.0.ML 
2 

3 
Compatibility wrapper for Poly/ML 5.0. 

4 
*) 

5 

28151
61f9c918b410
explicit use of universal.ML and dummy_thread.ML;
wenzelm
parents:
26378
diff
changeset

6 
use "MLSystems/universal.ML"; 
61f9c918b410
explicit use of universal.ML and dummy_thread.ML;
wenzelm
parents:
26378
diff
changeset

7 
use "MLSystems/thread_dummy.ML"; 
30672
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30627
diff
changeset

8 
use "MLSystems/ml_name_space.ML"; 
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
24605
diff
changeset

9 
use "MLSystems/polyml_common.ML"; 
31312  10 
use "MLSystems/compiler_polyml5.0.ML"; 
31313  11 
use "MLSystems/pp_polyml.ML"; 
21653  12 

13 
val pointer_eq = PolyML.pointerEq; 

21771
148c8aba89dd
added improved versions of use_text/file (still inactive);
wenzelm
parents:
21653
diff
changeset

14 

29638
1f8f3d26a2cf
added share_common_data  reduces heap space, but takes long;
wenzelm
parents:
29564
diff
changeset

15 
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; 
1f8f3d26a2cf
added share_common_data  reduces heap space, but takes long;
wenzelm
parents:
29564
diff
changeset

16 