renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
1 (* Title: Pure/pure_setup.ML
4 Pure theory and ML toplevel setup.
7 (* the Pure theories *)
9 val theory = ThyInfo.get_theory;
11 Context.>> (Context.map_theory
12 (Outer_Syntax.process_file (Path.explode "Pure.thy") #>
14 structure Pure = struct val thy = ML_Context.the_global_context () end;
15 Context.set_thread_data NONE;
16 ThyInfo.register_theory Pure.thy;
19 (* ML toplevel pretty printing *)
21 toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
22 toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
23 toplevel_pp ["Position", "T"] "Pretty.position";
24 toplevel_pp ["Binding", "binding"] "Pretty.str o quote o Binding.str_of";
25 toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm";
26 toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm";
27 toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp";
28 toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy";
29 toplevel_pp ["Context", "theory"] "Context.pretty_thy";
30 toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
31 toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
32 toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
33 toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
34 toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";
36 if ml_system = "polyml-5.3.0"
37 then use "ML-Systems/install_pp_polyml-5.3.ML"
38 else if String.isPrefix "polyml" ml_system
39 then use "ML-Systems/install_pp_polyml.ML"
42 if ml_system = "polyml-5.0" orelse ml_system = "polyml-5.1" then
43 Secure.use_text ML_Parse.global_context (0, "") false
44 "PolyML.Compiler.maxInlineSize := 20"
48 (* ML toplevel use commands *)
50 fun use name = Toplevel.program (fn () => ThyInfo.use name);
51 fun use_thys name = Toplevel.program (fn () => ThyInfo.use_thys name);
52 fun use_thy name = Toplevel.program (fn () => ThyInfo.use_thy name);
53 fun time_use name = Toplevel.program (fn () => ThyInfo.time_use name);
54 fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name);
59 val cd = File.cd o Path.explode;
61 Proofterm.proofs := 0;