author  wenzelm 
Sun, 31 May 2009 14:51:21 +0200  
changeset 31312  1c00e4ff3c99 
parent 30672  beaadd5af500 
child 31313  97800f7e80b4 
permissions  rwrr 
26381  1 
(* Title: Pure/MLSystems/polyml5.1.ML 
2 

3 
Compatibility wrapper for Poly/ML 5.1. 

4 
*) 

5 

28836  6 
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

7 
use "MLSystems/ml_name_space.ML"; 
26381  8 
use "MLSystems/polyml_common.ML"; 
31312  9 
use "MLSystems/compiler_polyml5.0.ML"; 
30627
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
29638
diff
changeset

10 
use "MLSystems/polyml_pp.ML"; 
26381  11 

12 
val pointer_eq = PolyML.pointerEq; 

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

13 

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

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

15 