added share_common_data -- reduces heap space, but takes long;
authorwenzelm
Tue Jan 27 12:59:22 2009 +0100 (2009-01-27)
changeset 296381f8f3d26a2cf
parent 29636 d01bada1df33
child 29639 b9a7ea6c6da7
added share_common_data -- reduces heap space, but takes long;
src/HOL/ROOT.ML
src/Pure/ML-Systems/polyml-5.0.ML
src/Pure/ML-Systems/polyml-5.1.ML
src/Pure/ML-Systems/polyml.ML
     1.1 --- a/src/HOL/ROOT.ML	Tue Jan 27 00:42:12 2009 +0100
     1.2 +++ b/src/HOL/ROOT.ML	Tue Jan 27 12:59:22 2009 +0100
     1.3 @@ -1,6 +1,7 @@
     1.4  (* Classical Higher-order Logic -- batteries included *)
     1.5  
     1.6  use_thy "Main";
     1.7 +share_common_data ();
     1.8  use_thy "Complex_Main";
     1.9  
    1.10  val HOL_proofs = ! Proofterm.proofs;
     2.1 --- a/src/Pure/ML-Systems/polyml-5.0.ML	Tue Jan 27 00:42:12 2009 +0100
     2.2 +++ b/src/Pure/ML-Systems/polyml-5.0.ML	Tue Jan 27 12:59:22 2009 +0100
     2.3 @@ -10,3 +10,5 @@
     2.4  
     2.5  val pointer_eq = PolyML.pointerEq;
     2.6  
     2.7 +fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
     2.8 +
     3.1 --- a/src/Pure/ML-Systems/polyml-5.1.ML	Tue Jan 27 00:42:12 2009 +0100
     3.2 +++ b/src/Pure/ML-Systems/polyml-5.1.ML	Tue Jan 27 12:59:22 2009 +0100
     3.3 @@ -8,3 +8,6 @@
     3.4  use "ML-Systems/polyml_old_compiler5.ML";
     3.5  
     3.6  val pointer_eq = PolyML.pointerEq;
     3.7 +
     3.8 +fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
     3.9 +
     4.1 --- a/src/Pure/ML-Systems/polyml.ML	Tue Jan 27 00:42:12 2009 +0100
     4.2 +++ b/src/Pure/ML-Systems/polyml.ML	Tue Jan 27 12:59:22 2009 +0100
     4.3 @@ -12,6 +12,8 @@
     4.4  
     4.5  val pointer_eq = PolyML.pointerEq;
     4.6  
     4.7 +fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
     4.8 +
     4.9  
    4.10  (* runtime compilation *)
    4.11