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@38217
|
7 |
(* the Pure theory *)
|
wenzelm@24053
|
8 |
|
wenzelm@26463
|
9 |
Context.>> (Context.map_theory
|
wenzelm@36953
|
10 |
(Outer_Syntax.process_file (Path.explode "Pure.thy") #>
|
wenzelm@26463
|
11 |
Theory.end_theory));
|
wenzelm@38217
|
12 |
|
wenzelm@26427
|
13 |
structure Pure = struct val thy = ML_Context.the_global_context () end;
|
wenzelm@38217
|
14 |
|
wenzelm@26427
|
15 |
Context.set_thread_data NONE;
|
wenzelm@38217
|
16 |
Thy_Info.register_thy Pure.thy;
|
wenzelm@23828
|
17 |
|
wenzelm@24053
|
18 |
|
wenzelm@24053
|
19 |
(* ML toplevel pretty printing *)
|
wenzelm@24053
|
20 |
|
wenzelm@37530
|
21 |
toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
|
wenzelm@30628
|
22 |
toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
|
wenzelm@30628
|
23 |
toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
|
wenzelm@30628
|
24 |
toplevel_pp ["Position", "T"] "Pretty.position";
|
wenzelm@43252
|
25 |
toplevel_pp ["Binding", "binding"] "Pretty.str o Binding.print";
|
wenzelm@33389
|
26 |
toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm";
|
wenzelm@33389
|
27 |
toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm";
|
wenzelm@33389
|
28 |
toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp";
|
wenzelm@33389
|
29 |
toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy";
|
wenzelm@30628
|
30 |
toplevel_pp ["Context", "theory"] "Context.pretty_thy";
|
wenzelm@30628
|
31 |
toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
|
wenzelm@33389
|
32 |
toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
|
wenzelm@43132
|
33 |
toplevel_pp ["Ast", "ast"] "Ast.pretty_ast";
|
wenzelm@44466
|
34 |
toplevel_pp ["Path", "T"] "Path.pretty";
|
wenzelm@42825
|
35 |
toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep";
|
wenzelm@38126
|
36 |
toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
|
wenzelm@38126
|
37 |
toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
|
wenzelm@24053
|
38 |
|
wenzelm@48994
|
39 |
if ML_System.is_polyml
|
wenzelm@38573
|
40 |
then use "ML/install_pp_polyml-5.3.ML"
|
wenzelm@33933
|
41 |
else ();
|
wenzelm@33933
|
42 |
|
wenzelm@24053
|
43 |
|
wenzelm@31646
|
44 |
(* ML toplevel use commands *)
|
wenzelm@31646
|
45 |
|
wenzelm@38212
|
46 |
fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name));
|
wenzelm@38212
|
47 |
|
wenzelm@37216
|
48 |
fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
|
wenzelm@37216
|
49 |
fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);
|
wenzelm@31646
|
50 |
|
wenzelm@31646
|
51 |
|
wenzelm@24053
|
52 |
(* misc *)
|
wenzelm@24053
|
53 |
|
wenzelm@23828
|
54 |
val cd = File.cd o Path.explode;
|
wenzelm@23828
|
55 |
|
wenzelm@25223
|
56 |
Proofterm.proofs := 0;
|
wenzelm@43231
|
57 |
|