author | wenzelm |
Sun, 29 Jul 2007 17:28:55 +0200 | |
changeset 24058 | 81aafd465662 |
parent 24053 | af1dd276fae0 |
child 24174 | 59a5ffec7078 |
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 time_use name = Toplevel.program (fn () => ThyInfo.time_use name); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
12 |
fun use_thys name = Toplevel.program (fn () => ThyInfo.use_thys name); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
13 |
fun use_thy name = Toplevel.program (fn () => ThyInfo.use_thy name); |
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 |
fun update_thy name = Toplevel.program (fn () => ThyInfo.update_thy name); |
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 |
|
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
18 |
(* the Pure theories *) |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
19 |
|
23828 | 20 |
use_thy "Pure"; |
21 |
structure Pure = struct val thy = theory "Pure" end; |
|
22 |
||
23 |
Context.add_setup |
|
24 |
(Sign.del_modesyntax Syntax.default_mode Syntax.appl_syntax #> |
|
25 |
Sign.add_syntax Syntax.applC_syntax); |
|
26 |
use_thy "CPure"; |
|
27 |
structure CPure = struct val thy = theory "CPure" end; |
|
28 |
||
24053
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
29 |
|
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
30 |
(* ML toplevel pretty printing *) |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
31 |
|
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
32 |
install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
33 |
install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
34 |
install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
35 |
install_pp (make_pp ["Context", "theory"] Context.pprint_thy); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
36 |
install_pp (make_pp ["Context", "proof"] ProofDisplay.pprint_context); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
37 |
install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
38 |
install_pp (make_pp ["typ"] (ProofDisplay.pprint_typ Pure.thy)); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
39 |
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
|
40 |
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
|
41 |
|
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
42 |
|
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
43 |
(* misc *) |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
44 |
|
23828 | 45 |
val cd = File.cd o Path.explode; |
46 |
ml_prompts "ML> " "ML# "; |
|
47 |
||
48 |
proofs := 0; |