isabelle: src/Pure/pure_setup.ML@aa533c5e3f48 (annotated)

23828 a8a3962f8eeb Pure theory setup. wenzelm parents: diff changeset	1	(* Title: Pure/pure_setup.ML
a8a3962f8eeb Pure theory setup. wenzelm parents: diff changeset	2	Author: Makarius
a8a3962f8eeb Pure theory setup. wenzelm parents: diff changeset	3
24053 af1dd276fae0 added ML toplevel use commands: Toplevel.program; wenzelm parents: 23828 diff changeset	4	Pure theory and ML toplevel setup.
23828 a8a3962f8eeb Pure theory setup. wenzelm parents: diff changeset	5	*)
a8a3962f8eeb Pure theory setup. wenzelm parents: diff changeset	6
37954 a2e73df0b1e0 simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants; wenzelm parents: 37949 diff changeset	7	(* the Pure theory *)
24053 af1dd276fae0 added ML toplevel use commands: Toplevel.program; wenzelm parents: 23828 diff changeset	8
26463 9283b4185fdf Context.>> : operate on Context.generic; wenzelm parents: 26435 diff changeset	9	Context.>> (Context.map_theory
36953 2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time; wenzelm parents: 33917 diff changeset	10	(Outer_Syntax.process_file (Path.explode "Pure.thy") #>
26463 9283b4185fdf Context.>> : operate on Context.generic; wenzelm parents: 26435 diff changeset	11	Theory.end_theory));
37954 a2e73df0b1e0 simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants; wenzelm parents: 37949 diff changeset	12
26427 f33d1b522316 implicit setup of emerging theory Pure; wenzelm parents: 25223 diff changeset	13	structure Pure = struct val thy = ML_Context.the_global_context () end;
37954 a2e73df0b1e0 simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants; wenzelm parents: 37949 diff changeset	14
26427 f33d1b522316 implicit setup of emerging theory Pure; wenzelm parents: 25223 diff changeset	15	Context.set_thread_data NONE;
37954 a2e73df0b1e0 simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants; wenzelm parents: 37949 diff changeset	16	Thy_Info.register_thy Pure.thy;
23828 a8a3962f8eeb Pure theory setup. wenzelm parents: diff changeset	17
24053 af1dd276fae0 added ML toplevel use commands: Toplevel.program; wenzelm parents: 23828 diff changeset	18
af1dd276fae0 added ML toplevel use commands: Toplevel.program; wenzelm parents: 23828 diff changeset	19	(* ML toplevel pretty printing *)
af1dd276fae0 added ML toplevel use commands: Toplevel.program; wenzelm parents: 23828 diff changeset	20
38470 484e483eb606 discontinued support for Poly/ML 5.0 and 5.1 versions; wenzelm parents: 38327 diff changeset	21	if String.isPrefix "polyml" ml_system
484e483eb606 discontinued support for Poly/ML 5.0 and 5.1 versions; wenzelm parents: 38327 diff changeset	22	then toplevel_pp ["String", "string"] "ML_Syntax.pretty_string"
484e483eb606 discontinued support for Poly/ML 5.0 and 5.1 versions; wenzelm parents: 38327 diff changeset	23	else ();
37860 aa3b3d00698b SML/NJ: refrain from modifying toplevel pp for type string -- unclear if it could work here; wenzelm parents: 37858 diff changeset	24
37529 a23e8aa853eb treat Pretty.T as strictly abstract type; wenzelm parents: 37216 diff changeset	25	toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
30625 d53d1a16d5ee replaced install_pp/make_pp by more general toplevel_pp based on use_text; wenzelm parents: 30621 diff changeset	26	toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
d53d1a16d5ee replaced install_pp/make_pp by more general toplevel_pp based on use_text; wenzelm parents: 30621 diff changeset	27	toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
d53d1a16d5ee replaced install_pp/make_pp by more general toplevel_pp based on use_text; wenzelm parents: 30621 diff changeset	28	toplevel_pp ["Position", "T"] "Pretty.position";
d53d1a16d5ee replaced install_pp/make_pp by more general toplevel_pp based on use_text; wenzelm parents: 30621 diff changeset	29	toplevel_pp ["Binding", "binding"] "Pretty.str o quote o Binding.str_of";
33389 bb3a5fa94a91 modernized structure Proof_Display; wenzelm parents: 33032 diff changeset	30	toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm";
bb3a5fa94a91 modernized structure Proof_Display; wenzelm parents: 33032 diff changeset	31	toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm";
bb3a5fa94a91 modernized structure Proof_Display; wenzelm parents: 33032 diff changeset	32	toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp";
bb3a5fa94a91 modernized structure Proof_Display; wenzelm parents: 33032 diff changeset	33	toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy";
30625 d53d1a16d5ee replaced install_pp/make_pp by more general toplevel_pp based on use_text; wenzelm parents: 30621 diff changeset	34	toplevel_pp ["Context", "theory"] "Context.pretty_thy";
d53d1a16d5ee replaced install_pp/make_pp by more general toplevel_pp based on use_text; wenzelm parents: 30621 diff changeset	35	toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
33389 bb3a5fa94a91 modernized structure Proof_Display; wenzelm parents: 33032 diff changeset	36	toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
30625 d53d1a16d5ee replaced install_pp/make_pp by more general toplevel_pp based on use_text; wenzelm parents: 30621 diff changeset	37	toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
d53d1a16d5ee replaced install_pp/make_pp by more general toplevel_pp based on use_text; wenzelm parents: 30621 diff changeset	38	toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
40741 17d6293a1e26 moved file identification to thy_load.ML (where it is actually used); wenzelm parents: 38470 diff changeset	39	toplevel_pp ["Thy_Load", "file_ident"] "Thy_Load.pretty_file_ident";
37858 e1ef6b441fe7 toplevel pp for Proof.state and Toplevel.state; wenzelm parents: 37535 diff changeset	40	toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
e1ef6b441fe7 toplevel pp for Proof.state and Toplevel.state; wenzelm parents: 37535 diff changeset	41	toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
24053 af1dd276fae0 added ML toplevel use commands: Toplevel.program; wenzelm parents: 23828 diff changeset	42
38470 484e483eb606 discontinued support for Poly/ML 5.0 and 5.1 versions; wenzelm parents: 38327 diff changeset	43	if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1"
38327 d6afb77b0f6d more precise and more maintainable dependencies; wenzelm parents: 37954 diff changeset	44	then use "ML/install_pp_polyml.ML"
38470 484e483eb606 discontinued support for Poly/ML 5.0 and 5.1 versions; wenzelm parents: 38327 diff changeset	45	else if String.isPrefix "polyml" ml_system
484e483eb606 discontinued support for Poly/ML 5.0 and 5.1 versions; wenzelm parents: 38327 diff changeset	46	then use "ML/install_pp_polyml-5.3.ML"
33917 186262d7cabf workaround for strange compiler crash of Poly/ML 5.0 and 5.1 at this point http://isabelle.in.tum.de/repos/isabelle/file/a2fc533175ff/src/HOL/Tools/Nitpick/nitpick_nut.ML#l997 wenzelm parents: 33538 diff changeset	47	else ();
186262d7cabf workaround for strange compiler crash of Poly/ML 5.0 and 5.1 at this point http://isabelle.in.tum.de/repos/isabelle/file/a2fc533175ff/src/HOL/Tools/Nitpick/nitpick_nut.ML#l997 wenzelm parents: 33538 diff changeset	48
24053 af1dd276fae0 added ML toplevel use commands: Toplevel.program; wenzelm parents: 23828 diff changeset	49
31646 ef30cd0e41e5 override toplevel "use" functions last; wenzelm parents: 31433 diff changeset	50	(* ML toplevel use commands *)
ef30cd0e41e5 override toplevel "use" functions last; wenzelm parents: 31433 diff changeset	51
37949 48a874444164 moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state; wenzelm parents: 37873 diff changeset	52	fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name));
48a874444164 moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state; wenzelm parents: 37873 diff changeset	53
37216 3165bc303f66 modernized some structure names, keeping a few legacy aliases; wenzelm parents: 36953 diff changeset	54	fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
3165bc303f66 modernized some structure names, keeping a few legacy aliases; wenzelm parents: 36953 diff changeset	55	fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);
31646 ef30cd0e41e5 override toplevel "use" functions last; wenzelm parents: 31433 diff changeset	56
ef30cd0e41e5 override toplevel "use" functions last; wenzelm parents: 31433 diff changeset	57
24053 af1dd276fae0 added ML toplevel use commands: Toplevel.program; wenzelm parents: 23828 diff changeset	58	(* misc *)
af1dd276fae0 added ML toplevel use commands: Toplevel.program; wenzelm parents: 23828 diff changeset	59
23828 a8a3962f8eeb Pure theory setup. wenzelm parents: diff changeset	60	val cd = File.cd o Path.explode;
a8a3962f8eeb Pure theory setup. wenzelm parents: diff changeset	61
25223 7463251e7273 qualified Proofterm.proofs; wenzelm parents: 24960 diff changeset	62	Proofterm.proofs := 0;

author	wenzelm
	Sun, 28 Nov 2010 15:28:48 +0100
changeset 40782	aa533c5e3f48
parent 40741	17d6293a1e26
child 41415	23533273220a
permissions	-rw-r--r--