# HG changeset patch # User wenzelm # Date 1374260199 -7200 # Node ID 155f02cacb2dec6b851a22d90c2e0c3a6d08c5ba # Parent 52790e3961fe016fa56caa1baea6081c08fe7b37 old Poly/ML 5.3.0 cannot share the massive heap of HOL anymore (after introduction of immutable theory in 38466f4f3483); diff -r 52790e3961fe -r 155f02cacb2d src/Pure/ML-Systems/polyml.ML --- a/src/Pure/ML-Systems/polyml.ML Fri Jul 19 17:58:57 2013 +0200 +++ b/src/Pure/ML-Systems/polyml.ML Fri Jul 19 20:56:39 2013 +0200 @@ -58,6 +58,10 @@ use "ML-Systems/ml_system.ML"; +if ML_System.name = "polyml-5.3.0" +then use "ML-Systems/share_common_data_polyml-5.3.0.ML" +else (); + structure ML_System = struct diff -r 52790e3961fe -r 155f02cacb2d src/Pure/ML-Systems/share_common_data_polyml-5.3.0.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML-Systems/share_common_data_polyml-5.3.0.ML Fri Jul 19 20:56:39 2013 +0200 @@ -0,0 +1,11 @@ +(* Title: Pure/ML-Systems/share_common_data_polyml-5.3.0.ML + +Dummy for Poly/ML 5.3.0, which cannot share the massive heap of HOL +anymore. +*) + +structure PolyML = +struct + open PolyML; + fun shareCommonData _ = (); +end; diff -r 52790e3961fe -r 155f02cacb2d src/Pure/ROOT --- a/src/Pure/ROOT Fri Jul 19 17:58:57 2013 +0200 +++ b/src/Pure/ROOT Fri Jul 19 20:56:39 2013 +0200 @@ -16,6 +16,7 @@ "ML-Systems/proper_int.ML" "ML-Systems/single_assignment.ML" "ML-Systems/single_assignment_polyml.ML" + "ML-Systems/share_common_data_polyml-5.3.0.ML" "ML-Systems/smlnj.ML" "ML-Systems/thread_dummy.ML" "ML-Systems/universal.ML"