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

author	wenzelm
	Tue, 20 Aug 2019 14:55:27 +0200
changeset 70589	00b67aaa4010
parent 68918	3a0db30e5d87
child 76670	b04d45bebbc5
permissions	-rw-r--r--