wenzelm@23828
|
1 |
(* Title: Pure/pure_setup.ML
|
wenzelm@23828
|
2 |
Author: Makarius
|
wenzelm@23828
|
3 |
|
wenzelm@24053
|
4 |
Pure theory and ML toplevel setup.
|
wenzelm@23828
|
5 |
*)
|
wenzelm@23828
|
6 |
|
wenzelm@24053
|
7 |
(* the Pure theories *)
|
wenzelm@24053
|
8 |
|
wenzelm@26608
|
9 |
val theory = ThyInfo.get_theory;
|
wenzelm@26608
|
10 |
|
wenzelm@26463
|
11 |
Context.>> (Context.map_theory
|
wenzelm@36953
|
12 |
(Outer_Syntax.process_file (Path.explode "Pure.thy") #>
|
wenzelm@26463
|
13 |
Theory.end_theory));
|
wenzelm@26427
|
14 |
structure Pure = struct val thy = ML_Context.the_global_context () end;
|
wenzelm@26427
|
15 |
Context.set_thread_data NONE;
|
wenzelm@26427
|
16 |
ThyInfo.register_theory Pure.thy;
|
wenzelm@23828
|
17 |
|
wenzelm@24053
|
18 |
|
wenzelm@24053
|
19 |
(* ML toplevel pretty printing *)
|
wenzelm@24053
|
20 |
|
wenzelm@30628
|
21 |
toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
|
wenzelm@30628
|
22 |
toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
|
wenzelm@30628
|
23 |
toplevel_pp ["Position", "T"] "Pretty.position";
|
wenzelm@30628
|
24 |
toplevel_pp ["Binding", "binding"] "Pretty.str o quote o Binding.str_of";
|
wenzelm@33389
|
25 |
toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm";
|
wenzelm@33389
|
26 |
toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm";
|
wenzelm@33389
|
27 |
toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp";
|
wenzelm@33389
|
28 |
toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy";
|
wenzelm@30628
|
29 |
toplevel_pp ["Context", "theory"] "Context.pretty_thy";
|
wenzelm@30628
|
30 |
toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
|
wenzelm@33389
|
31 |
toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
|
wenzelm@30628
|
32 |
toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
|
wenzelm@30628
|
33 |
toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
|
wenzelm@30628
|
34 |
toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";
|
wenzelm@24053
|
35 |
|
wenzelm@33540
|
36 |
if ml_system = "polyml-5.3.0"
|
wenzelm@31437
|
37 |
then use "ML-Systems/install_pp_polyml-5.3.ML"
|
wenzelm@30628
|
38 |
else if String.isPrefix "polyml" ml_system
|
wenzelm@30628
|
39 |
then use "ML-Systems/install_pp_polyml.ML"
|
wenzelm@28557
|
40 |
else ();
|
wenzelm@28557
|
41 |
|
wenzelm@33933
|
42 |
if ml_system = "polyml-5.0" orelse ml_system = "polyml-5.1" then
|
wenzelm@33933
|
43 |
Secure.use_text ML_Parse.global_context (0, "") false
|
wenzelm@33933
|
44 |
"PolyML.Compiler.maxInlineSize := 20"
|
wenzelm@33933
|
45 |
else ();
|
wenzelm@33933
|
46 |
|
wenzelm@24053
|
47 |
|
wenzelm@31646
|
48 |
(* ML toplevel use commands *)
|
wenzelm@31646
|
49 |
|
wenzelm@33032
|
50 |
fun use name = Toplevel.program (fn () => ThyInfo.use name);
|
wenzelm@33032
|
51 |
fun use_thys name = Toplevel.program (fn () => ThyInfo.use_thys name);
|
wenzelm@33032
|
52 |
fun use_thy name = Toplevel.program (fn () => ThyInfo.use_thy name);
|
wenzelm@33032
|
53 |
fun time_use name = Toplevel.program (fn () => ThyInfo.time_use name);
|
wenzelm@31646
|
54 |
fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name);
|
wenzelm@31646
|
55 |
|
wenzelm@31646
|
56 |
|
wenzelm@24053
|
57 |
(* misc *)
|
wenzelm@24053
|
58 |
|
wenzelm@23828
|
59 |
val cd = File.cd o Path.explode;
|
wenzelm@23828
|
60 |
|
wenzelm@25223
|
61 |
Proofterm.proofs := 0;
|