isabelle: src/Pure/ML_Bootstrap.thy@844c067bc3d4 (annotated)

62887 6b2c60ebd915 clarified ML bootstrap environment; wenzelm parents: 62883 diff changeset	1	(* Title: Pure/ML_Bootstrap.thy
62868 61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	2	Author: Makarius
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	3
62887 6b2c60ebd915 clarified ML bootstrap environment; wenzelm parents: 62883 diff changeset	4	ML bootstrap environment -- with access to low-level structures!
62868 61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	5	*)
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	6
62887 6b2c60ebd915 clarified ML bootstrap environment; wenzelm parents: 62883 diff changeset	7	theory ML_Bootstrap
62880 76e7d9169b54 clarified files; wenzelm parents: 62873 diff changeset	8	imports Pure
62868 61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	9	begin
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	10
62944 3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	11	subsection \<open>Standard ML environment for virtual bootstrap\<close>
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	12
62873 2f9c8a18f832 support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML; wenzelm parents: 62871 diff changeset	13	setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
62930 51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: 62902 diff changeset	14
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: 62902 diff changeset	15	SML_import \<open>
62944 3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	16	structure Output_Primitives = Output_Primitives_Virtual;
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	17	structure Thread_Data = Thread_Data_Virtual;
64331 abf7b6e6865f proper type for Poly/ML development version; wenzelm parents: 63220 diff changeset	18	fun ML_system_pp (_: FixedInt.int -> 'a -> 'b -> PolyML_Pretty.pretty) = ();
62930 51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: 62902 diff changeset	19	\<close>
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: 62902 diff changeset	20
62944 3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	21
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	22	subsection \<open>Final setup of global ML environment\<close>
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	23
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	24	ML \<open>Proofterm.proofs := 0\<close>
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	25
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	26	ML \<open>
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	27	Context.setmp_generic_context NONE
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	28	ML \<open>
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	29	List.app ML_Name_Space.forget_structure ML_Name_Space.hidden_structures;
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	30	structure PolyML = struct structure IntInf = PolyML.IntInf end;
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	31	\<close>
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	32	\<close>
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	33
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	34	ML \<open>@{assert} (not (can ML \<open>open RunCall\<close>))\<close>
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	35
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	36
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	37	subsection \<open>Switch to bootstrap environment\<close>
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	38
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62893 diff changeset	39	setup \<open>Config.put_global ML_Env.SML_environment true\<close>
62868 61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	40
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	41	end

author	wenzelm
	Tue, 14 Mar 2017 11:16:23 +0100
changeset 65223	844c067bc3d4
parent 64331	abf7b6e6865f
child 67105	05ff3e6dbbce
permissions	-rw-r--r--