author | wenzelm |
Mon, 22 Sep 2008 15:26:11 +0200 | |
changeset 28317 | 83c4fc383409 |
parent 28179 | 8e8313aededc |
child 28414 | 419954d26886 |
permissions | -rw-r--r-- |
23828 | 1 |
(* Title: Pure/pure_setup.ML |
2 |
ID: $Id$ |
|
3 |
Author: Makarius |
|
4 |
||
24053
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
5 |
Pure theory and ML toplevel setup. |
23828 | 6 |
*) |
7 |
||
24053
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
8 |
(* ML toplevel use commands *) |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
9 |
|
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
10 |
fun use name = Toplevel.program (fn () => ThyInfo.use name); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
11 |
fun use_thys name = Toplevel.program (fn () => ThyInfo.use_thys name); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
12 |
fun use_thy name = Toplevel.program (fn () => ThyInfo.use_thy name); |
24174
59a5ffec7078
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24053
diff
changeset
|
13 |
fun time_use name = Toplevel.program (fn () => ThyInfo.time_use name); |
24053
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
14 |
fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
15 |
|
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
16 |
|
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
17 |
(* the Pure theories *) |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
18 |
|
26608 | 19 |
val theory = ThyInfo.get_theory; |
20 |
||
26463 | 21 |
Context.>> (Context.map_theory |
22 |
(OuterSyntax.process_file (Path.explode "Pure.thy") #> |
|
23 |
Theory.end_theory)); |
|
26427 | 24 |
structure Pure = struct val thy = ML_Context.the_global_context () end; |
25 |
Context.set_thread_data NONE; |
|
26 |
ThyInfo.register_theory Pure.thy; |
|
23828 | 27 |
|
24053
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
28 |
|
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
29 |
(* ML toplevel pretty printing *) |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
30 |
|
28179 | 31 |
install_pp (make_pp ["TaskQueue", "task"] (Pretty.pprint o Pretty.str o TaskQueue.str_of_task)); |
32 |
install_pp (make_pp ["TaskQueue", "group"] (Pretty.pprint o Pretty.str o TaskQueue.str_of_group)); |
|
27776 | 33 |
install_pp (make_pp ["Position", "T"] (Pretty.pprint o Pretty.enum "," "{" "}" o |
34 |
map (fn (x, y) => Pretty.str (x ^ "=" ^ y)) o Position.properties_of)); |
|
24053
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
35 |
install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
36 |
install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
37 |
install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
38 |
install_pp (make_pp ["Context", "theory"] Context.pprint_thy); |
27341 | 39 |
install_pp (make_pp ["Context", "theory_ref"] Context.pprint_thy_ref); |
24053
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
40 |
install_pp (make_pp ["Context", "proof"] ProofDisplay.pprint_context); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
41 |
install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
42 |
install_pp (make_pp ["typ"] (ProofDisplay.pprint_typ Pure.thy)); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
43 |
install_pp (make_pp ["Path", "T"] (Pretty.pprint o Pretty.str o quote o Path.implode)); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
44 |
install_pp (make_pp ["File", "ident"] (Pretty.pprint o Pretty.str o quote o File.rep_ident)); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
45 |
|
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
46 |
|
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
47 |
(* misc *) |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
48 |
|
23828 | 49 |
val cd = File.cd o Path.explode; |
50 |
ml_prompts "ML> " "ML# "; |
|
51 |
||
25223 | 52 |
Proofterm.proofs := 0; |