isabelle: src/Pure/ML_Bootstrap.thy@fca40adc6342 (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	keywords "use" "use_debug" "use_no_debug" :: thy_load
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	10	begin
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	11
62873 2f9c8a18f832 support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML; wenzelm parents: 62871 diff changeset	12	setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
62893 fca40adc6342 virtual thread data via context, for proper support of Context.>> etc; wenzelm parents: 62887 diff changeset	13	SML_import \<open>structure Thread_Data = Thread_Data_Virtual\<close>
62873 2f9c8a18f832 support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML; wenzelm parents: 62871 diff changeset	14
62868 61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	15	ML \<open>
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	16	local
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	17
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	18	val _ =
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	19	Outer_Syntax.command @{command_keyword use}
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	20	"read and evaluate Isabelle/ML or SML file"
62871 4a6cbe1239fe proper syntax; wenzelm parents: 62868 diff changeset	21	(Resources.parse_files "use" --\| @{keyword ";"} >> ML_File.use NONE);
62868 61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	22
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	23	val _ =
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	24	Outer_Syntax.command @{command_keyword use_debug}
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	25	"read and evaluate Isabelle/ML or SML file (with debugger information)"
62871 4a6cbe1239fe proper syntax; wenzelm parents: 62868 diff changeset	26	(Resources.parse_files "use_debug" --\| @{keyword ";"} >> ML_File.use (SOME true));
62868 61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	27
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	28	val _ =
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	29	Outer_Syntax.command @{command_keyword use_no_debug}
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	30	"read and evaluate Isabelle/ML or SML file (no debugger information)"
62871 4a6cbe1239fe proper syntax; wenzelm parents: 62868 diff changeset	31	(Resources.parse_files "use_no_debug" --\| @{keyword ";"} >> ML_File.use (SOME false));
62868 61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	32
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	33	in end
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	34	\<close>
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	35
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	36	end

author	wenzelm
	Wed, 06 Apr 2016 19:03:29 +0200
changeset 62893	fca40adc6342
parent 62887	6b2c60ebd915
child 62902	3c0f53eae166
permissions	-rw-r--r--