isabelle: src/Pure/ML-Systems/polyml-5.2.ML@f76ad0771f67 (annotated)

33538 edf497b5b5d2 setup for official Poly/ML 5.3.0, which is now the default; wenzelm parents: 32776 diff changeset	1	(* Title: Pure/ML-Systems/polyml-5.2.ML
2341 e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x). wenzelm parents: diff changeset	2
33538 edf497b5b5d2 setup for official Poly/ML 5.3.0, which is now the default; wenzelm parents: 32776 diff changeset	3	Compatibility wrapper for Poly/ML 5.2.
2341 e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x). wenzelm parents: diff changeset	4	*)
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x). wenzelm parents: diff changeset	5
32776 1504f9c2d060 more uniform treatment of structure Unsynchronized in ML bootstrap phase; wenzelm parents: 32294 diff changeset	6	use "ML-Systems/unsynchronized.ML";
1504f9c2d060 more uniform treatment of structure Unsynchronized in ML bootstrap phase; wenzelm parents: 32294 diff changeset	7
28152 c1277547d59f * empty log message * wenzelm parents: 28125 diff changeset	8	open Thread;
30672 beaadd5af500 more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context; wenzelm parents: 30627 diff changeset	9
beaadd5af500 more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context; wenzelm parents: 30627 diff changeset	10	structure ML_Name_Space =
beaadd5af500 more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context; wenzelm parents: 30627 diff changeset	11	struct
beaadd5af500 more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context; wenzelm parents: 30627 diff changeset	12	open PolyML.NameSpace;
beaadd5af500 more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context; wenzelm parents: 30627 diff changeset	13	type T = PolyML.NameSpace.nameSpace;
beaadd5af500 more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context; wenzelm parents: 30627 diff changeset	14	val global = PolyML.globalNameSpace;
beaadd5af500 more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context; wenzelm parents: 30627 diff changeset	15	end;
beaadd5af500 more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context; wenzelm parents: 30627 diff changeset	16
31427 5a07cc86675d reraise exceptions to preserve original position (ML system specific); wenzelm parents: 31313 diff changeset	17	fun reraise exn = raise exn;
5a07cc86675d reraise exceptions to preserve original position (ML system specific); wenzelm parents: 31313 diff changeset	18
26215 94d32a7cd0fb rearrangements to make latest Poly/ML the default, not old 4.x; wenzelm parents: 26084 diff changeset	19	use "ML-Systems/polyml_common.ML";
28676 78688a5fafc2 multithreading support only for polyml-5.2.1 or later; wenzelm parents: 28268 diff changeset	20
33538 edf497b5b5d2 setup for official Poly/ML 5.3.0, which is now the default; wenzelm parents: 32776 diff changeset	21	use "ML-Systems/thread_dummy.ML";
edf497b5b5d2 setup for official Poly/ML 5.3.0, which is now the default; wenzelm parents: 32776 diff changeset	22	use "ML-Systems/multithreading.ML";
26215 94d32a7cd0fb rearrangements to make latest Poly/ML the default, not old 4.x; wenzelm parents: 26084 diff changeset	23
94d32a7cd0fb rearrangements to make latest Poly/ML the default, not old 4.x; wenzelm parents: 26084 diff changeset	24	val pointer_eq = PolyML.pointerEq;
23921 947152add153 added compatibility file for ML systems without multithreading; wenzelm parents: 23826 diff changeset	25
29638 1f8f3d26a2cf added share_common_data -- reduces heap space, but takes long; wenzelm parents: 29564 diff changeset	26	fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
1f8f3d26a2cf added share_common_data -- reduces heap space, but takes long; wenzelm parents: 29564 diff changeset	27
31312 1c00e4ff3c99 more modular setup of runtime compilation; wenzelm parents: 30672 diff changeset	28	use "ML-Systems/compiler_polyml-5.2.ML";
31313 97800f7e80b4 renamed polyml_pp.ML to pp_polyml.ML; wenzelm parents: 31312 diff changeset	29	use "ML-Systems/pp_polyml.ML";
38635 f76ad0771f67 added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later); wenzelm parents: 33538 diff changeset	30	use "ML-Systems/pp_dummy.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	31

author	wenzelm
	Mon, 23 Aug 2010 15:11:41 +0200
changeset 38635	f76ad0771f67
parent 33538	edf497b5b5d2
child 39616	8052101883c3
permissions	-rw-r--r--