isabelle: src/Pure/ML_Bootstrap.thy@0004e7a9fa10 (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
67105 05ff3e6dbbce clarified dependencies: "isabelle build -S" should be invariant wrt. change of ML system or platform; wenzelm parents: 64331 diff changeset	11	external_file "$POLYML_EXE"
05ff3e6dbbce clarified dependencies: "isabelle build -S" should be invariant wrt. change of ML system or platform; wenzelm parents: 64331 diff changeset	12
05ff3e6dbbce clarified dependencies: "isabelle build -S" should be invariant wrt. change of ML system or platform; wenzelm parents: 64331 diff changeset	13
62944 3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	14	subsection \<open>Standard ML environment for virtual bootstrap\<close>
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	15
62873 2f9c8a18f832 support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML; wenzelm parents: 62871 diff changeset	16	setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
62930 51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: 62902 diff changeset	17
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: 62902 diff changeset	18	SML_import \<open>
62944 3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	19	structure Output_Primitives = Output_Primitives_Virtual;
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	20	structure Thread_Data = Thread_Data_Virtual;
64331 abf7b6e6865f proper type for Poly/ML development version; wenzelm parents: 63220 diff changeset	21	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	22	\<close>
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: 62902 diff changeset	23
62944 3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	24
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	25	subsection \<open>Final setup of global ML environment\<close>
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	26
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	27	ML \<open>Proofterm.proofs := 0\<close>
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	28
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	29	ML \<open>
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	30	Context.setmp_generic_context NONE
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	31	ML \<open>
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	32	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	33	structure PolyML = struct structure IntInf = PolyML.IntInf end;
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	34	\<close>
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	35	\<close>
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	36
67147 dea94b1aabc3 prefer control symbol antiquotations; wenzelm parents: 67105 diff changeset	37	ML \<open>\<^assert> (not (can ML \<open>open RunCall\<close>))\<close>
62944 3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	38
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	39
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	40	subsection \<open>Switch to bootstrap environment\<close>
3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	41
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62893 diff changeset	42	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	43
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	44	end

author	wenzelm
	Sun, 20 May 2018 15:37:16 +0200
changeset 68231	0004e7a9fa10
parent 67147	dea94b1aabc3
child 68803	169bf32b35dd
permissions	-rw-r--r--