wenzelm@23828
|
1 |
(* Title: Pure/pure_setup.ML
|
wenzelm@23828
|
2 |
ID: $Id$
|
wenzelm@23828
|
3 |
Author: Makarius
|
wenzelm@23828
|
4 |
|
wenzelm@24053
|
5 |
Pure theory and ML toplevel setup.
|
wenzelm@23828
|
6 |
*)
|
wenzelm@23828
|
7 |
|
wenzelm@24053
|
8 |
(* ML toplevel use commands *)
|
wenzelm@24053
|
9 |
|
wenzelm@24053
|
10 |
fun use name = Toplevel.program (fn () => ThyInfo.use name);
|
wenzelm@24053
|
11 |
fun use_thys name = Toplevel.program (fn () => ThyInfo.use_thys name);
|
wenzelm@24053
|
12 |
fun use_thy name = Toplevel.program (fn () => ThyInfo.use_thy name);
|
wenzelm@24174
|
13 |
fun time_use name = Toplevel.program (fn () => ThyInfo.time_use name);
|
wenzelm@24053
|
14 |
fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name);
|
wenzelm@24053
|
15 |
|
wenzelm@24053
|
16 |
|
wenzelm@24053
|
17 |
(* the Pure theories *)
|
wenzelm@24053
|
18 |
|
wenzelm@26608
|
19 |
val theory = ThyInfo.get_theory;
|
wenzelm@26608
|
20 |
|
wenzelm@26463
|
21 |
Context.>> (Context.map_theory
|
wenzelm@26463
|
22 |
(OuterSyntax.process_file (Path.explode "Pure.thy") #>
|
wenzelm@26463
|
23 |
Theory.end_theory));
|
wenzelm@26427
|
24 |
structure Pure = struct val thy = ML_Context.the_global_context () end;
|
wenzelm@26427
|
25 |
Context.set_thread_data NONE;
|
wenzelm@26427
|
26 |
ThyInfo.register_theory Pure.thy;
|
wenzelm@23828
|
27 |
|
wenzelm@24053
|
28 |
|
wenzelm@24053
|
29 |
(* ML toplevel pretty printing *)
|
wenzelm@24053
|
30 |
|
wenzelm@28179
|
31 |
install_pp (make_pp ["TaskQueue", "task"] (Pretty.pprint o Pretty.str o TaskQueue.str_of_task));
|
wenzelm@28179
|
32 |
install_pp (make_pp ["TaskQueue", "group"] (Pretty.pprint o Pretty.str o TaskQueue.str_of_group));
|
wenzelm@27776
|
33 |
install_pp (make_pp ["Position", "T"] (Pretty.pprint o Pretty.enum "," "{" "}" o
|
wenzelm@27776
|
34 |
map (fn (x, y) => Pretty.str (x ^ "=" ^ y)) o Position.properties_of));
|
wenzelm@24053
|
35 |
install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);
|
wenzelm@24053
|
36 |
install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm);
|
wenzelm@24053
|
37 |
install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp);
|
wenzelm@24053
|
38 |
install_pp (make_pp ["Context", "theory"] Context.pprint_thy);
|
wenzelm@27341
|
39 |
install_pp (make_pp ["Context", "theory_ref"] Context.pprint_thy_ref);
|
wenzelm@24053
|
40 |
install_pp (make_pp ["Context", "proof"] ProofDisplay.pprint_context);
|
wenzelm@24053
|
41 |
install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast);
|
wenzelm@24053
|
42 |
install_pp (make_pp ["typ"] (ProofDisplay.pprint_typ Pure.thy));
|
wenzelm@24053
|
43 |
install_pp (make_pp ["Path", "T"] (Pretty.pprint o Pretty.str o quote o Path.implode));
|
wenzelm@24053
|
44 |
install_pp (make_pp ["File", "ident"] (Pretty.pprint o Pretty.str o quote o File.rep_ident));
|
wenzelm@24053
|
45 |
|
wenzelm@28557
|
46 |
if String.isPrefix "polyml" ml_system then use "ML-Systems/install_pp_polyml.ML"
|
wenzelm@28557
|
47 |
else ();
|
wenzelm@28557
|
48 |
|
wenzelm@24053
|
49 |
|
wenzelm@24053
|
50 |
(* misc *)
|
wenzelm@24053
|
51 |
|
wenzelm@23828
|
52 |
val cd = File.cd o Path.explode;
|
wenzelm@23828
|
53 |
ml_prompts "ML> " "ML# ";
|
wenzelm@23828
|
54 |
|
wenzelm@25223
|
55 |
Proofterm.proofs := 0;
|