author | wenzelm |
Tue, 08 Nov 2005 10:44:40 +0100 | |
changeset 18124 | a310c78298f9 |
parent 17900 | 5f44c71c4ca4 |
child 18358 | 0a733e11021a |
permissions | -rw-r--r-- |
5830 | 1 |
(* Title: Pure/Isar/isar_thy.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
||
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
5 |
Derived theory and proof operations. |
5830 | 6 |
*) |
7 |
||
8 |
signature ISAR_THY = |
|
9 |
sig |
|
15703 | 10 |
val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory |
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
11 |
val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory |
15703 | 12 |
val add_defs: bool * ((bstring * string) * Attrib.src list) list -> theory -> theory |
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
13 |
val add_defs_i: bool * ((bstring * term) * theory attribute list) list -> theory -> theory |
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
14 |
val apply_theorems: (thmref * Attrib.src list) list -> theory -> theory * thm list |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
15 |
val apply_theorems_i: (thm list * theory attribute list) list -> theory -> theory * thm list |
15703 | 16 |
val theorems: string -> |
17 |
((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list |
|
12713
c9e3e34dbc45
clarified/added theorems(_i) vs. locale_theorems(_i);
wenzelm
parents:
12705
diff
changeset
|
18 |
-> theory -> theory * (string * thm list) list |
c9e3e34dbc45
clarified/added theorems(_i) vs. locale_theorems(_i);
wenzelm
parents:
12705
diff
changeset
|
19 |
val theorems_i: string -> |
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
20 |
((bstring * theory attribute list) * (thm list * theory attribute list) list) list |
12713
c9e3e34dbc45
clarified/added theorems(_i) vs. locale_theorems(_i);
wenzelm
parents:
12705
diff
changeset
|
21 |
-> theory -> theory * (string * thm list) list |
c9e3e34dbc45
clarified/added theorems(_i) vs. locale_theorems(_i);
wenzelm
parents:
12705
diff
changeset
|
22 |
val smart_theorems: string -> xstring option -> |
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
23 |
((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list -> |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
24 |
theory -> theory * Proof.context |
15703 | 25 |
val declare_theorems: xstring option -> |
17108 | 26 |
(thmref * Attrib.src list) list -> theory -> theory * Proof.context |
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
27 |
val have: ((string * Attrib.src list) * (string * (string list * string list)) list) list -> |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
28 |
bool -> Proof.state -> Proof.state |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
29 |
val hence: ((string * Attrib.src list) * (string * (string list * string list)) list) list -> |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
30 |
bool -> Proof.state -> Proof.state |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
31 |
val show: ((string * Attrib.src list) * (string * (string list * string list)) list) list -> |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
32 |
bool -> Proof.state -> Proof.state |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
33 |
val thus: ((string * Attrib.src list) * (string * (string list * string list)) list) list -> |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
34 |
bool -> Proof.state -> Proof.state |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
35 |
val theorem: string -> string * Attrib.src list -> string * (string list * string list) -> |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
36 |
theory -> Proof.state |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
37 |
val theorem_i: string -> string * theory attribute list -> term * (term list * term list) -> |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
38 |
theory -> Proof.state |
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
39 |
val qed: Method.text option -> Toplevel.transition -> Toplevel.transition |
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
40 |
val terminal_proof: Method.text * Method.text option -> |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
41 |
Toplevel.transition -> Toplevel.transition |
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
42 |
val default_proof: Toplevel.transition -> Toplevel.transition |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
43 |
val immediate_proof: Toplevel.transition -> Toplevel.transition |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
44 |
val done_proof: Toplevel.transition -> Toplevel.transition |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
45 |
val skip_proof: Toplevel.transition -> Toplevel.transition |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
46 |
val forget_proof: Toplevel.transition -> Toplevel.transition |
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
47 |
val begin_theory: string -> string list -> (string * bool) list -> bool -> theory |
6331 | 48 |
val end_theory: theory -> theory |
7932 | 49 |
val kill_theory: string -> unit |
6246 | 50 |
val theory: string * string list * (string * bool) list |
51 |
-> Toplevel.transition -> Toplevel.transition |
|
7960 | 52 |
val init_context: ('a -> unit) -> 'a -> Toplevel.transition -> Toplevel.transition |
6246 | 53 |
val context: string -> Toplevel.transition -> Toplevel.transition |
5830 | 54 |
end; |
55 |
||
56 |
structure IsarThy: ISAR_THY = |
|
57 |
struct |
|
58 |
||
59 |
(* axioms and defs *) |
|
60 |
||
5915 | 61 |
fun add_axms f args thy = |
62 |
f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy; |
|
63 |
||
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
64 |
val add_axioms = add_axms (#1 oo PureThy.add_axioms); |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
65 |
val add_axioms_i = #1 oo PureThy.add_axioms_i; |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
66 |
fun add_defs (x, args) = add_axms (#1 oo PureThy.add_defs x) args; |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
67 |
fun add_defs_i (x, args) = (#1 oo PureThy.add_defs_i x) args; |
6371 | 68 |
|
69 |
||
5915 | 70 |
(* theorems *) |
71 |
||
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
72 |
fun present_theorems kind (thy, named_thmss) = |
17108 | 73 |
conditional (kind <> "" andalso kind <> Drule.internalK) (fn () => |
15531 | 74 |
Context.setmp (SOME thy) (Present.results (kind ^ "s")) named_thmss); |
17108 | 75 |
|
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
76 |
fun theorems kind args thy = thy |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
77 |
|> PureThy.note_thmss (Drule.kind kind) (Attrib.map_facts (Attrib.global_attribute thy) args) |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
78 |
|> tap (present_theorems kind); |
12713
c9e3e34dbc45
clarified/added theorems(_i) vs. locale_theorems(_i);
wenzelm
parents:
12705
diff
changeset
|
79 |
|
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
80 |
fun theorems_i kind args = |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
81 |
PureThy.note_thmss_i (Drule.kind kind) args |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
82 |
#> tap (present_theorems kind); |
9590 | 83 |
|
15570 | 84 |
fun apply_theorems args = apsnd (List.concat o map snd) o theorems "" [(("", []), args)]; |
85 |
fun apply_theorems_i args = apsnd (List.concat o map snd) o theorems_i "" [(("", []), args)]; |
|
6371 | 86 |
|
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
87 |
fun smart_theorems kind NONE args thy = thy |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
88 |
|> theorems kind args |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
89 |
|> tap (present_theorems kind) |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
90 |
|> (fn (thy, _) => (thy, ProofContext.init thy)) |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
91 |
| smart_theorems kind (SOME loc) args thy = thy |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
92 |
|> Locale.note_thmss kind loc args |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
93 |
|> tap (present_theorems kind o apfst #1) |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
94 |
|> #1; |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
95 |
|
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
96 |
fun declare_theorems opt_loc args = |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
97 |
smart_theorems "" opt_loc [(("", []), args)]; |
12705 | 98 |
|
5915 | 99 |
|
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
100 |
(* goals *) |
10935 | 101 |
|
102 |
local |
|
103 |
||
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
104 |
fun local_goal opt_chain goal stmt int = |
18124 | 105 |
opt_chain #> goal NONE (K Seq.single) stmt int; |
12244 | 106 |
|
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
107 |
fun global_goal goal kind a propp thy = |
18124 | 108 |
goal kind NONE (K I) (SOME "") a [(("", []), [propp])] (ProofContext.init thy); |
10935 | 109 |
|
110 |
in |
|
111 |
||
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
112 |
val have = local_goal I Proof.have; |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
113 |
val hence = local_goal Proof.chain Proof.have; |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
114 |
val show = local_goal I Proof.show; |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
115 |
val thus = local_goal Proof.chain Proof.show; |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
116 |
val theorem = global_goal Proof.theorem; |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
117 |
val theorem_i = global_goal Proof.theorem_i; |
11890 | 118 |
|
7271 | 119 |
end; |
120 |
||
5830 | 121 |
|
6404 | 122 |
(* local endings *) |
123 |
||
17900 | 124 |
fun local_qed m = Toplevel.proofs (Proof.local_qed (m, true)); |
125 |
val local_terminal_proof = Toplevel.proofs o Proof.local_terminal_proof; |
|
126 |
val local_default_proof = Toplevel.proofs Proof.local_default_proof; |
|
127 |
val local_immediate_proof = Toplevel.proofs Proof.local_immediate_proof; |
|
128 |
val local_done_proof = Toplevel.proofs Proof.local_done_proof; |
|
129 |
val local_skip_proof = Toplevel.proofs' Proof.local_skip_proof; |
|
16605
4590c1f79050
added print_mode three_buffersN and corresponding cond_print;
wenzelm
parents:
16529
diff
changeset
|
130 |
|
15237
250e9be7a09d
Some changes to allow skipping of proof scripts.
berghofe
parents:
15206
diff
changeset
|
131 |
val skip_local_qed = |
250e9be7a09d
Some changes to allow skipping of proof scripts.
berghofe
parents:
15206
diff
changeset
|
132 |
Toplevel.skip_proof (History.apply (fn i => if i > 1 then i - 1 else raise Toplevel.UNDEF)); |
6404 | 133 |
|
134 |
||
135 |
(* global endings *) |
|
136 |
||
17900 | 137 |
fun global_ending ending = Toplevel.proof_to_theory_context (fn int => fn state => |
138 |
(Proof.assert_bottom true state handle Proof.STATE _ => raise Toplevel.UNDEF; |
|
139 |
ending int state)); |
|
6404 | 140 |
|
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
141 |
fun global_qed m = global_ending (K (Proof.global_qed (m, true))); |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
142 |
val global_terminal_proof = global_ending o K o Proof.global_terminal_proof; |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
143 |
val global_default_proof = global_ending (K Proof.global_default_proof); |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
144 |
val global_immediate_proof = global_ending (K Proof.global_immediate_proof); |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
145 |
val global_skip_proof = global_ending Proof.global_skip_proof; |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
146 |
val global_done_proof = global_ending (K Proof.global_done_proof); |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
147 |
|
17900 | 148 |
val skip_global_qed = Toplevel.skip_proof_to_theory (equal 1); |
6404 | 149 |
|
150 |
||
151 |
(* common endings *) |
|
152 |
||
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
153 |
fun qed m = local_qed m o global_qed m o skip_local_qed o skip_global_qed; |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
154 |
fun terminal_proof m = local_terminal_proof m o global_terminal_proof m; |
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
155 |
val default_proof = local_default_proof o global_default_proof; |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
156 |
val immediate_proof = local_immediate_proof o global_immediate_proof; |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
157 |
val done_proof = local_done_proof o global_done_proof; |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
158 |
val skip_proof = local_skip_proof o global_skip_proof; |
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
159 |
|
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
160 |
val forget_proof = |
17900 | 161 |
Toplevel.proof_to_theory Proof.theory_of o |
15237
250e9be7a09d
Some changes to allow skipping of proof scripts.
berghofe
parents:
15206
diff
changeset
|
162 |
Toplevel.skip_proof_to_theory (K true); |
8210 | 163 |
|
5830 | 164 |
|
6688 | 165 |
(* theory init and exit *) |
5830 | 166 |
|
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
167 |
fun begin_theory name imports uses = |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
168 |
ThyInfo.begin_theory Present.begin_theory name imports (map (apfst Path.unpack) uses); |
5830 | 169 |
|
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
170 |
val end_theory = (ThyInfo.check_known_thy o Context.theory_name) ? ThyInfo.end_theory; |
7909 | 171 |
|
7932 | 172 |
val kill_theory = ThyInfo.if_known_thy ThyInfo.remove_thy; |
6688 | 173 |
|
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
174 |
fun theory (name, imports, uses) = |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
175 |
Toplevel.init_theory (begin_theory name imports uses) |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
176 |
(fn thy => (end_theory thy; ())) |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
177 |
(kill_theory o Context.theory_name); |
6246 | 178 |
|
179 |
||
180 |
(* context switch *) |
|
181 |
||
7960 | 182 |
fun fetch_context f x = |
15531 | 183 |
(case Context.pass NONE f x of |
184 |
((), NONE) => raise Toplevel.UNDEF |
|
185 |
| ((), SOME thy) => thy); |
|
7960 | 186 |
|
187 |
fun init_context f x = Toplevel.init_theory (fn _ => fetch_context f x) (K ()) (K ()); |
|
7953 | 188 |
|
189 |
val context = init_context (ThyInfo.quiet_update_thy true); |
|
6246 | 190 |
|
5830 | 191 |
end; |