isabelle: src/Pure/ML_Bootstrap.thy@34e0ddfc6dcc (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
68816 5a53724fe247 support named ML environments, notably "Isabelle", "SML"; wenzelm parents: 68812 diff changeset	11	ML \<open>
5a53724fe247 support named ML environments, notably "Isabelle", "SML"; wenzelm parents: 68812 diff changeset	12	#allStruct ML_Name_Space.global () \|> List.app (fn (name, _) =>
5a53724fe247 support named ML environments, notably "Isabelle", "SML"; wenzelm parents: 68812 diff changeset	13	if member (op =) ML_Name_Space.hidden_structures name then
5a53724fe247 support named ML environments, notably "Isabelle", "SML"; wenzelm parents: 68812 diff changeset	14	ML (Input.string ("structure " ^ name ^ " = " ^ name))
5a53724fe247 support named ML environments, notably "Isabelle", "SML"; wenzelm parents: 68812 diff changeset	15	else ());
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;
68816 5a53724fe247 support named ML environments, notably "Isabelle", "SML"; wenzelm parents: 68812 diff changeset	18	structure PolyML = PolyML;
68918 3a0db30e5d87 simplified signature (again, see 751bcf0473a7): e.g. relevant for non-Isabelle ML environments; wenzelm parents: 68819 diff changeset	19	fun ML_system_pp (_: FixedInt.int -> 'a -> 'b -> PolyML.pretty) = ();
62944 3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	20
68819 9cfa4aa35719 tuned; wenzelm parents: 68816 diff changeset	21	Proofterm.proofs := 0;
62944 3ee643c5ed00 more standard session build process, including browser_info; wenzelm parents: 62930 diff changeset	22
68816 5a53724fe247 support named ML environments, notably "Isabelle", "SML"; wenzelm parents: 68812 diff changeset	23	Context.setmp_generic_context NONE
5a53724fe247 support named ML environments, notably "Isabelle", "SML"; wenzelm parents: 68812 diff changeset	24	ML \<open>
5a53724fe247 support named ML environments, notably "Isabelle", "SML"; wenzelm parents: 68812 diff changeset	25	List.app ML_Name_Space.forget_structure ML_Name_Space.hidden_structures;
5a53724fe247 support named ML environments, notably "Isabelle", "SML"; wenzelm parents: 68812 diff changeset	26	structure PolyML =
5a53724fe247 support named ML environments, notably "Isabelle", "SML"; wenzelm parents: 68812 diff changeset	27	struct
5a53724fe247 support named ML environments, notably "Isabelle", "SML"; wenzelm parents: 68812 diff changeset	28	val pointerEq = pointer_eq;
5a53724fe247 support named ML environments, notably "Isabelle", "SML"; wenzelm parents: 68812 diff changeset	29	structure IntInf = PolyML.IntInf;
68918 3a0db30e5d87 simplified signature (again, see 751bcf0473a7): e.g. relevant for non-Isabelle ML environments; wenzelm parents: 68819 diff changeset	30	datatype context = datatype PolyML.context;
3a0db30e5d87 simplified signature (again, see 751bcf0473a7): e.g. relevant for non-Isabelle ML environments; wenzelm parents: 68819 diff changeset	31	datatype pretty = datatype PolyML.pretty;
68816 5a53724fe247 support named ML environments, notably "Isabelle", "SML"; wenzelm parents: 68812 diff changeset	32	end;
5a53724fe247 support named ML environments, notably "Isabelle", "SML"; wenzelm parents: 68812 diff changeset	33	\<close>
62944 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
68816 5a53724fe247 support named ML environments, notably "Isabelle", "SML"; wenzelm parents: 68812 diff changeset	36	setup \<open>Context.theory_map ML_Env.bootstrap_name_space\<close>
68819 9cfa4aa35719 tuned; wenzelm parents: 68816 diff changeset	37
78728 72631efa3821 explicitly reject 'handle' with catch-all patterns; wenzelm parents: 76670 diff changeset	38	declare [[ML_read_global = false, ML_catch_all = true]]
62868 61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	39
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	40	end

author	paulson <lp15@cam.ac.uk>
	Mon, 22 Apr 2024 22:08:28 +0100
changeset 80142	34e0ddfc6dcc
parent 78728	72631efa3821
permissions	-rw-r--r--