author | wenzelm |
Mon, 13 Aug 2007 18:10:19 +0200 | |
changeset 24242 | e52ef498c0ba |
parent 24174 | 59a5ffec7078 |
child 24960 | 39d1dd215d73 |
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 |
|
23828 | 19 |
use_thy "Pure"; |
20 |
structure Pure = struct val thy = theory "Pure" end; |
|
21 |
||
22 |
Context.add_setup |
|
24242 | 23 |
(Sign.del_modesyntax_i Syntax.default_mode PureThy.appl_syntax #> |
24 |
Sign.add_syntax_i PureThy.applC_syntax); |
|
23828 | 25 |
use_thy "CPure"; |
26 |
structure CPure = struct val thy = theory "CPure" end; |
|
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 |
|
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
31 |
install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
32 |
install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
33 |
install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
34 |
install_pp (make_pp ["Context", "theory"] Context.pprint_thy); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
35 |
install_pp (make_pp ["Context", "proof"] ProofDisplay.pprint_context); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
36 |
install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
37 |
install_pp (make_pp ["typ"] (ProofDisplay.pprint_typ Pure.thy)); |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
38 |
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
|
39 |
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
|
40 |
|
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 |
(* misc *) |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
43 |
|
23828 | 44 |
val cd = File.cd o Path.explode; |
45 |
ml_prompts "ML> " "ML# "; |
|
46 |
||
47 |
proofs := 0; |