author  wenzelm 
Sat, 09 Dec 2006 18:05:44 +0100  
changeset 21725  ec2014c93d7f 
parent 21663  734a9c3f562d 
child 21858  05f57309170c 
permissions  rwrr 
5831  1 
(* Title: Pure/Isar/isar_cmd.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

21350  5 
Derived Isar commands. 
5831  6 
*) 
7 

8 
signature ISAR_CMD = 

9 
sig 

21350  10 
val add_axioms: ((bstring * string) * Attrib.src list) list > theory > theory 
11 
val add_defs: (bool * bool) * ((bstring * string) * Attrib.src list) list > theory > theory 

12 
val apply_theorems: (thmref * Attrib.src list) list > theory > thm list * theory 

13 
val apply_theorems_i: (thm list * attribute list) list > theory > thm list * theory 

14 
val have: ((string * Attrib.src list) * (string * string list) list) list > 

15 
bool > Proof.state > Proof.state 

16 
val hence: ((string * Attrib.src list) * (string * string list) list) list > 

17 
bool > Proof.state > Proof.state 

18 
val show: ((string * Attrib.src list) * (string * string list) list) list > 

19 
bool > Proof.state > Proof.state 

20 
val thus: ((string * Attrib.src list) * (string * string list) list) list > 

21 
bool > Proof.state > Proof.state 

22 
val qed: Method.text option > Toplevel.transition > Toplevel.transition 

23 
val terminal_proof: Method.text * Method.text option > 

24 
Toplevel.transition > Toplevel.transition 

25 
val default_proof: Toplevel.transition > Toplevel.transition 

26 
val immediate_proof: Toplevel.transition > Toplevel.transition 

27 
val done_proof: Toplevel.transition > Toplevel.transition 

28 
val skip_proof: Toplevel.transition > Toplevel.transition 

29 
val begin_theory: string > string list > (string * bool) list > bool > theory 

30 
val end_theory: theory > theory 

31 
val kill_theory: string > unit 

32 
val theory: string * string list * (string * bool) list 

33 
> Toplevel.transition > Toplevel.transition 

34 
val init_context: ('a > unit) > 'a > Toplevel.transition > Toplevel.transition 

7462  35 
val welcome: Toplevel.transition > Toplevel.transition 
36 
val init_toplevel: Toplevel.transition > Toplevel.transition 

5831  37 
val exit: Toplevel.transition > Toplevel.transition 
38 
val quit: Toplevel.transition > Toplevel.transition 

7908  39 
val touch_child_thys: string > Toplevel.transition > Toplevel.transition 
7101  40 
val touch_all_thys: Toplevel.transition > Toplevel.transition 
41 
val touch_thy: string > Toplevel.transition > Toplevel.transition 

42 
val remove_thy: string > Toplevel.transition > Toplevel.transition 

7931  43 
val kill_thy: string > Toplevel.transition > Toplevel.transition 
9731  44 
val pr: string list * (int option * int option) > Toplevel.transition > Toplevel.transition 
8453  45 
val disable_pr: Toplevel.transition > Toplevel.transition 
46 
val enable_pr: Toplevel.transition > Toplevel.transition 

20978  47 
val cannot_undo: string > Toplevel.transition > Toplevel.transition 
7729  48 
val clear_undos_theory: int > Toplevel.transition > Toplevel.transition 
6742  49 
val redo: Toplevel.transition > Toplevel.transition 
50 
val undos_proof: int > Toplevel.transition > Toplevel.transition 

7936  51 
val kill_proof_notify: (unit > unit) > Toplevel.transition > Toplevel.transition 
6742  52 
val kill_proof: Toplevel.transition > Toplevel.transition 
53 
val undo_theory: Toplevel.transition > Toplevel.transition 

6686  54 
val undo: Toplevel.transition > Toplevel.transition 
8498  55 
val kill: Toplevel.transition > Toplevel.transition 
17066  56 
val back: Toplevel.transition > Toplevel.transition 
14950  57 
val use: Path.T > Toplevel.transition > Toplevel.transition 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12758
diff
changeset

58 
val use_mltext_theory: string > Toplevel.transition > Toplevel.transition 
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12758
diff
changeset

59 
val use_mltext: bool > string > Toplevel.transition > Toplevel.transition 
5831  60 
val use_commit: Toplevel.transition > Toplevel.transition 
14950  61 
val cd: Path.T > Toplevel.transition > Toplevel.transition 
5831  62 
val pwd: Toplevel.transition > Toplevel.transition 
63 
val use_thy: string > Toplevel.transition > Toplevel.transition 

6694  64 
val use_thy_only: string > Toplevel.transition > Toplevel.transition 
6195  65 
val update_thy: string > Toplevel.transition > Toplevel.transition 
7101  66 
val update_thy_only: string > Toplevel.transition > Toplevel.transition 
14950  67 
val display_drafts: Path.T list > Toplevel.transition > Toplevel.transition 
68 
val print_drafts: Path.T list > Toplevel.transition > Toplevel.transition 

7124  69 
val pretty_setmargin: int > Toplevel.transition > Toplevel.transition 
7308  70 
val print_context: Toplevel.transition > Toplevel.transition 
20621  71 
val print_theory: bool > Toplevel.transition > Toplevel.transition 
5831  72 
val print_syntax: Toplevel.transition > Toplevel.transition 
21725  73 
val print_abbrevs: Toplevel.transition > Toplevel.transition 
21003
37492b0062c6
renamed print_lthms to print_facts, do not insist on proof state;
wenzelm
parents:
20978
diff
changeset

74 
val print_facts: Toplevel.transition > Toplevel.transition 
5880  75 
val print_theorems: Toplevel.transition > Toplevel.transition 
12060  76 
val print_locales: Toplevel.transition > Toplevel.transition 
18135  77 
val print_locale: bool * (Locale.expr * Element.context list) 
12758  78 
> Toplevel.transition > Toplevel.transition 
17139
165c97f9bb63
Printing of interpretations: option to show witness theorems;
ballarin
parents:
17066
diff
changeset

79 
val print_registrations: bool > string > Toplevel.transition > Toplevel.transition 
5831  80 
val print_attributes: Toplevel.transition > Toplevel.transition 
16026  81 
val print_simpset: Toplevel.transition > Toplevel.transition 
12382  82 
val print_rules: Toplevel.transition > Toplevel.transition 
11666  83 
val print_induct_rules: Toplevel.transition > Toplevel.transition 
9219  84 
val print_trans_rules: Toplevel.transition > Toplevel.transition 
5831  85 
val print_methods: Toplevel.transition > Toplevel.transition 
9219  86 
val print_antiquotations: Toplevel.transition > Toplevel.transition 
20574  87 
val class_deps: Toplevel.transition > Toplevel.transition 
88 
val thm_deps: (thmref * Attrib.src list) list > Toplevel.transition > Toplevel.transition 

16037  89 
val find_theorems: int option * (bool * string FindTheorems.criterion) list 
13284  90 
> Toplevel.transition > Toplevel.transition 
5831  91 
val print_binds: Toplevel.transition > Toplevel.transition 
8369  92 
val print_cases: Toplevel.transition > Toplevel.transition 
19268  93 
val print_stmts: string list * (thmref * Attrib.src list) list 
94 
> Toplevel.transition > Toplevel.transition 

15703  95 
val print_thms: string list * (thmref * Attrib.src list) list 
10581  96 
> Toplevel.transition > Toplevel.transition 
15703  97 
val print_prfs: bool > string list * (thmref * Attrib.src list) list option 
11524
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11017
diff
changeset

98 
> Toplevel.transition > Toplevel.transition 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12758
diff
changeset

99 
val print_prop: (string list * string) > Toplevel.transition > Toplevel.transition 
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12758
diff
changeset

100 
val print_term: (string list * string) > Toplevel.transition > Toplevel.transition 
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12758
diff
changeset

101 
val print_type: (string list * string) > Toplevel.transition > Toplevel.transition 
12938
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

102 
val add_header: string * Position.T > Toplevel.transition > Toplevel.transition 
17262
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

103 
val add_chapter: xstring option * (string * Position.T) > 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

104 
Toplevel.transition > Toplevel.transition 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

105 
val add_section: xstring option * (string * Position.T) > 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

106 
Toplevel.transition > Toplevel.transition 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

107 
val add_subsection: xstring option * (string * Position.T) > 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

108 
Toplevel.transition > Toplevel.transition 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

109 
val add_subsubsection: xstring option * (string * Position.T) > 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

110 
Toplevel.transition > Toplevel.transition 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

111 
val add_text: xstring option * (string * Position.T) > 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

112 
Toplevel.transition > Toplevel.transition 
12938
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

113 
val add_text_raw: string * Position.T > Toplevel.transition > Toplevel.transition 
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

114 
val add_sect: string * Position.T > Toplevel.transition > Toplevel.transition 
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

115 
val add_subsect: string * Position.T > Toplevel.transition > Toplevel.transition 
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

116 
val add_subsubsect: string * Position.T > Toplevel.transition > Toplevel.transition 
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

117 
val add_txt: string * Position.T > Toplevel.transition > Toplevel.transition 
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

118 
val add_txt_raw: string * Position.T > Toplevel.transition > Toplevel.transition 
5831  119 
end; 
120 

121 
structure IsarCmd: ISAR_CMD = 

122 
struct 

123 

124 

21350  125 
(* axioms *) 
126 

127 
fun add_axms f args thy = 

128 
f (map (fn (x, srcs) => (x, map (Attrib.attribute thy) srcs)) args) thy; 

129 

130 
val add_axioms = add_axms (snd oo PureThy.add_axioms); 

131 

132 
fun add_defs ((unchecked, overloaded), args) = 

133 
add_axms 

134 
(snd oo (if unchecked then PureThy.add_defs_unchecked else PureThy.add_defs) overloaded) args; 

135 

136 

137 
(* facts *) 

138 

139 
fun apply_theorems args thy = 

140 
let val facts = Attrib.map_facts (Attrib.attribute thy) [(("", []), args)] 

141 
in apfst (maps snd) (PureThy.note_thmss "" facts thy) end; 

142 

143 
fun apply_theorems_i args = apfst (maps snd) o PureThy.note_thmss_i "" [(("", []), args)]; 

144 

145 

146 
(* goals *) 

147 

148 
fun goal opt_chain goal stmt int = 

149 
opt_chain #> goal NONE (K Seq.single) stmt int; 

150 

151 
val have = goal I Proof.have; 

152 
val hence = goal Proof.chain Proof.have; 

153 
val show = goal I Proof.show; 

154 
val thus = goal Proof.chain Proof.show; 

155 

156 

157 
(* local endings *) 

158 

159 
fun local_qed m = Toplevel.proofs (Proof.local_qed (m, true)); 

160 
val local_terminal_proof = Toplevel.proofs o Proof.local_terminal_proof; 

161 
val local_default_proof = Toplevel.proofs Proof.local_default_proof; 

162 
val local_immediate_proof = Toplevel.proofs Proof.local_immediate_proof; 

163 
val local_done_proof = Toplevel.proofs Proof.local_done_proof; 

164 
val local_skip_proof = Toplevel.proofs' Proof.local_skip_proof; 

165 

166 
val skip_local_qed = 

167 
Toplevel.skip_proof (History.apply (fn i => if i > 1 then i  1 else raise Toplevel.UNDEF)); 

168 

169 

170 
(* global endings *) 

171 

172 
fun global_qed m = Toplevel.end_proof (K (Proof.global_qed (m, true))); 

173 
val global_terminal_proof = Toplevel.end_proof o K o Proof.global_terminal_proof; 

174 
val global_default_proof = Toplevel.end_proof (K Proof.global_default_proof); 

175 
val global_immediate_proof = Toplevel.end_proof (K Proof.global_immediate_proof); 

176 
val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof; 

177 
val global_done_proof = Toplevel.end_proof (K Proof.global_done_proof); 

178 

179 
val skip_global_qed = Toplevel.skip_proof_to_theory (equal 1); 

180 

181 

182 
(* common endings *) 

183 

184 
fun qed m = local_qed m o global_qed m o skip_local_qed o skip_global_qed; 

185 
fun terminal_proof m = local_terminal_proof m o global_terminal_proof m; 

186 
val default_proof = local_default_proof o global_default_proof; 

187 
val immediate_proof = local_immediate_proof o global_immediate_proof; 

188 
val done_proof = local_done_proof o global_done_proof; 

189 
val skip_proof = local_skip_proof o global_skip_proof; 

190 

191 

192 
(* init and exit *) 

193 

194 
fun begin_theory name imports uses = 

195 
ThyInfo.begin_theory Present.begin_theory name imports (map (apfst Path.unpack) uses); 

196 

21566  197 
fun end_theory thy = 
198 
if ThyInfo.check_known_thy (Context.theory_name thy) then ThyInfo.end_theory thy else thy; 

21350  199 

200 
val kill_theory = ThyInfo.if_known_thy ThyInfo.remove_thy; 

201 

202 
fun theory (name, imports, uses) = 

203 
Toplevel.init_theory (begin_theory name imports uses) 

204 
(fn thy => (end_theory thy; ())) 

205 
(kill_theory o Context.theory_name); 

206 

207 
fun init_context f x = Toplevel.init_theory 

208 
(fn _ => 

209 
(case Context.pass NONE f x of 

210 
((), NONE) => raise Toplevel.UNDEF 

211 
 ((), SOME thy) => thy)) 

212 
(K ()) (K ()); 

7462  213 

214 
val init_toplevel = Toplevel.imperative (fn () => raise Toplevel.RESTART); 

21350  215 

7462  216 
val welcome = Toplevel.imperative (writeln o Session.welcome); 
5831  217 

218 
val exit = Toplevel.keep (fn state => 

21725  219 
(Context.set_context (try Toplevel.theory_of state); raise Toplevel.TERMINATE)); 
5831  220 

221 
val quit = Toplevel.imperative quit; 

222 

7101  223 

224 
(* touch theories *) 

225 

7908  226 
fun touch_child_thys name = Toplevel.imperative (fn () => ThyInfo.touch_child_thys name); 
7101  227 
val touch_all_thys = Toplevel.imperative ThyInfo.touch_all_thys; 
228 
fun touch_thy name = Toplevel.imperative (fn () => ThyInfo.touch_thy name); 

229 
fun remove_thy name = Toplevel.imperative (fn () => ThyInfo.remove_thy name); 

21350  230 
fun kill_thy name = Toplevel.imperative (fn () => kill_theory name); 
7101  231 

5831  232 

8453  233 
(* print state *) 
234 

8463  235 
fun with_modes modes e = 
236 
Library.setmp print_mode (modes @ ! print_mode) e (); 

237 

15531  238 
fun set_limit _ NONE = () 
239 
 set_limit r (SOME n) = r := n; 

9731  240 

19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

241 
fun pr (modes, (lim1, lim2)) = Toplevel.keep (fn state => 
9731  242 
(set_limit goals_limit lim1; set_limit ProofContext.prems_limit lim2; Toplevel.quiet := false; 
19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

243 
with_modes modes (fn () => Toplevel.print_state true state))); 
8453  244 

245 
val disable_pr = Toplevel.imperative (fn () => Toplevel.quiet := true); 

246 
val enable_pr = Toplevel.imperative (fn () => Toplevel.quiet := false); 

247 

248 

6686  249 
(* history commands *) 
250 

20978  251 
fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt)); 
252 

7729  253 
val clear_undos_theory = Toplevel.history o History.clear; 
16812  254 

255 
val redo = 

256 
Toplevel.history History.redo o 

257 
Toplevel.actual_proof ProofHistory.redo o 

15237
250e9be7a09d
Some changes to allow skipping of proof scripts.
berghofe
parents:
15222
diff
changeset

258 
Toplevel.skip_proof History.redo; 
6686  259 

16812  260 
fun undos_proof n = 
261 
Toplevel.actual_proof (fn prf => 

15237
250e9be7a09d
Some changes to allow skipping of proof scripts.
berghofe
parents:
15222
diff
changeset

262 
if ProofHistory.is_initial prf then raise Toplevel.UNDEF else funpow n ProofHistory.undo prf) o 
250e9be7a09d
Some changes to allow skipping of proof scripts.
berghofe
parents:
15222
diff
changeset

263 
Toplevel.skip_proof (fn h => 
250e9be7a09d
Some changes to allow skipping of proof scripts.
berghofe
parents:
15222
diff
changeset

264 
if History.is_initial h then raise Toplevel.UNDEF else funpow n History.undo h); 
6686  265 

7936  266 
fun kill_proof_notify (f: unit > unit) = Toplevel.history (fn hist => 
18588  267 
if is_some (Toplevel.theory_node (History.current hist)) then raise Toplevel.UNDEF 
268 
else (f (); History.undo hist)); 

7936  269 

270 
val kill_proof = kill_proof_notify (K ()); 

6686  271 

6742  272 
val undo_theory = Toplevel.history (fn hist => 
273 
if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist); 

6686  274 

7413  275 
val undo = Toplevel.kill o undo_theory o undos_proof 1; 
21003
37492b0062c6
renamed print_lthms to print_facts, do not insist on proof state;
wenzelm
parents:
20978
diff
changeset

276 
val kill = Toplevel.kill o kill_proof; 
17899  277 

278 
val back = 

279 
Toplevel.actual_proof ProofHistory.back o 

280 
Toplevel.skip_proof (History.apply I); 

9273  281 

6686  282 

5831  283 
(* use ML text *) 
284 

16045  285 
fun use path = Toplevel.keep (fn state => 
286 
Context.setmp (try Toplevel.theory_of state) (ThyInfo.load_file false) path); 

5831  287 

288 
(*passes changes of theory context*) 

12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12758
diff
changeset

289 
val use_mltext_theory = Toplevel.theory' o Context.use_mltext_theory; 
5831  290 

291 
(*ignore result theory context*) 

12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12758
diff
changeset

292 
fun use_mltext v txt = Toplevel.keep' (fn verb => fn state => 
8349
611342539639
moved use_mltext, use_mltext_theory, use_let, use_setup to context.ML;
wenzelm
parents:
7936
diff
changeset

293 
(Context.use_mltext txt (v andalso verb) (try Toplevel.theory_of state))); 
5831  294 

20927  295 
val use_commit = Toplevel.imperative Secure.commit; 
5831  296 

297 

298 
(* current working directory *) 

299 

14950  300 
fun cd path = Toplevel.imperative (fn () => (File.cd path)); 
7790  301 
val pwd = Toplevel.imperative (fn () => writeln (Path.pack (File.pwd ()))); 
5831  302 

303 

304 
(* load theory files *) 

305 

6243  306 
fun use_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy name); 
6694  307 
fun use_thy_only name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy_only name); 
6243  308 
fun update_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.update_thy name); 
7124  309 
fun update_thy_only name = 
310 
Toplevel.imperative (fn () => Context.save ThyInfo.update_thy_only name); 

311 

312 

14934  313 
(* present draft files *) 
314 

315 
fun display_drafts files = Toplevel.imperative (fn () => 

16258  316 
let val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files) 
317 
in File.isatool ("display c " ^ outfile ^ " &"); () end); 

14934  318 

319 
fun print_drafts files = Toplevel.imperative (fn () => 

16258  320 
let val outfile = File.shell_path (Present.drafts "ps" files) 
321 
in File.isatool ("print c " ^ outfile); () end); 

14934  322 

323 

7124  324 
(* pretty_setmargin *) 
325 

326 
fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.setmargin n); 

5831  327 

328 

9513  329 
(* print parts of theory and proof context *) 
5831  330 

7308  331 
val print_context = Toplevel.keep Toplevel.print_state_context; 
9513  332 

20621  333 
fun print_theory verbose = Toplevel.unknown_theory o 
334 
Toplevel.keep (ProofDisplay.print_full_theory verbose o Toplevel.theory_of); 

9513  335 

21663  336 
val print_syntax = Toplevel.unknown_context o 
337 
Toplevel.keep (ProofContext.print_syntax o Toplevel.context_of); 

9513  338 

21725  339 
val print_abbrevs = Toplevel.unknown_context o 
340 
Toplevel.keep (ProofContext.print_abbrevs o Toplevel.context_of); 

341 

21003
37492b0062c6
renamed print_lthms to print_facts, do not insist on proof state;
wenzelm
parents:
20978
diff
changeset

342 
val print_facts = Toplevel.unknown_context o Toplevel.keep (fn state => 
37492b0062c6
renamed print_lthms to print_facts, do not insist on proof state;
wenzelm
parents:
20978
diff
changeset

343 
ProofContext.setmp_verbose 
21506  344 
ProofContext.print_lthms (Toplevel.context_of state)); 
21003
37492b0062c6
renamed print_lthms to print_facts, do not insist on proof state;
wenzelm
parents:
20978
diff
changeset

345 

17066  346 
val print_theorems_proof = Toplevel.keep (fn state => 
347 
ProofContext.setmp_verbose 

348 
ProofContext.print_lthms (Proof.context_of (Toplevel.proof_of state))); 

349 

18588  350 
val print_theorems_theory = Toplevel.keep (fn state => 
351 
Toplevel.theory_of state > 

352 
(case Option.map Toplevel.theory_node (History.previous (Toplevel.node_history_of state)) of 

20957  353 
SOME (SOME prev_thy) => ProofDisplay.print_theorems_diff (Context.theory_of prev_thy) 
19430  354 
 _ => ProofDisplay.print_theorems)); 
18588  355 

21663  356 
val print_theorems = Toplevel.unknown_context o print_theorems_theory o print_theorems_proof; 
9513  357 

12060  358 
val print_locales = Toplevel.unknown_theory o 
359 
Toplevel.keep (Locale.print_locales o Toplevel.theory_of); 

360 

19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

361 
fun print_locale (show_facts, (import, body)) = Toplevel.unknown_theory o 
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

362 
Toplevel.keep (fn state => 
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

363 
Locale.print_locale (Toplevel.theory_of state) show_facts import body); 
15596  364 

17139
165c97f9bb63
Printing of interpretations: option to show witness theorems;
ballarin
parents:
17066
diff
changeset

365 
fun print_registrations show_wits name = Toplevel.unknown_context o 
20957  366 
Toplevel.keep (Toplevel.node_case 
367 
(Context.cases (Locale.print_global_registrations show_wits name) 

368 
(Locale.print_local_registrations show_wits name)) 

17139
165c97f9bb63
Printing of interpretations: option to show witness theorems;
ballarin
parents:
17066
diff
changeset

369 
(Locale.print_local_registrations show_wits name o Proof.context_of)); 
12060  370 

9513  371 
val print_attributes = Toplevel.unknown_theory o 
372 
Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of); 

373 

16026  374 
val print_simpset = Toplevel.unknown_context o 
20957  375 
Toplevel.keep (Toplevel.node_case 
376 
(Context.cases Simplifier.print_simpset Simplifier.print_local_simpset) 

16026  377 
(Simplifier.print_local_simpset o Proof.context_of)); 
378 

12382  379 
val print_rules = Toplevel.unknown_context o 
18639  380 
Toplevel.keep (ContextRules.print_rules o Toplevel.context_of); 
12382  381 

11666  382 
val print_induct_rules = Toplevel.unknown_context o 
18639  383 
Toplevel.keep (InductAttrib.print_rules o Toplevel.context_of); 
11666  384 

9513  385 
val print_trans_rules = Toplevel.unknown_context o 
18639  386 
Toplevel.keep (Calculation.print_rules o Toplevel.context_of); 
9513  387 

388 
val print_methods = Toplevel.unknown_theory o 

389 
Toplevel.keep (Method.print_methods o Toplevel.theory_of); 

390 

9219  391 
val print_antiquotations = Toplevel.imperative IsarOutput.print_antiquotations; 
5831  392 

20574  393 
val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state => 
394 
let 

395 
val thy = Toplevel.theory_of state; 

396 
val {classes = (space, algebra), ...} = Type.rep_tsig (Sign.tsig_of thy); 

397 
val {classes, ...} = Sorts.rep_algebra algebra; 

398 
fun entry (c, (i, (_, cs))) = 

399 
(i, {name = NameSpace.extern space c, ID = c, parents = cs, 

400 
dir = "", unfold = true, path = ""}); 

401 
val gr = 

402 
Graph.fold (cons o entry) classes [] 

403 
> sort (int_ord o pairself #1) > map #2; 

404 
in Present.display_graph gr end); 

405 

15964
f2074e12d1d4
searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
kleing
parents:
15799
diff
changeset

406 

16026  407 
(* retrieve theorems *) 
7615  408 

9513  409 
fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state => 
21003
37492b0062c6
renamed print_lthms to print_facts, do not insist on proof state;
wenzelm
parents:
20978
diff
changeset

410 
ThmDeps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args)); 
9454  411 

16026  412 
fun find_theorems (opt_lim, spec) = Toplevel.unknown_theory o Toplevel.keep (fn state => 
413 
let 

21003
37492b0062c6
renamed print_lthms to print_facts, do not insist on proof state;
wenzelm
parents:
20978
diff
changeset

414 
val proof_state = Toplevel.enter_proof_body state; 
16026  415 
val ctxt = Proof.context_of proof_state; 
416 
val opt_goal = try Proof.get_goal proof_state > Option.map (Thm.prop_of o #2 o #2); 

417 
in FindTheorems.print_theorems ctxt opt_goal opt_lim spec end); 

418 

5831  419 

420 
(* print proof context contents *) 

421 

21663  422 
val print_binds = Toplevel.unknown_context o Toplevel.keep (fn state => 
423 
ProofContext.setmp_verbose ProofContext.print_binds (Toplevel.context_of state)); 

9513  424 

21663  425 
val print_cases = Toplevel.unknown_context o Toplevel.keep (fn state => 
426 
ProofContext.setmp_verbose ProofContext.print_cases (Toplevel.context_of state)); 

5831  427 

428 

19268  429 
(* print theorems, terms, types etc. *) 
430 

19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

431 
local 
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

432 

c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

433 
fun string_of_stmts state args = 
19268  434 
Proof.get_thmss state args 
21437  435 
> map (Element.pretty_statement (Proof.context_of state) Thm.theoremK) 
19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

436 
> Pretty.chunks2 > Pretty.string_of; 
5880  437 

19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

438 
fun string_of_thms state args = 
12055  439 
Pretty.string_of (ProofContext.pretty_thms (Proof.context_of state) 
19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

440 
(Proof.get_thmss state args)); 
5895  441 

19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

442 
fun string_of_prfs full state arg = 
17066  443 
Pretty.string_of (case arg of 
15531  444 
NONE => 
12125
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

445 
let 
17066  446 
val (ctxt, (_, thm)) = Proof.get_goal state; 
447 
val {thy, der = (_, prf), ...} = Thm.rep_thm thm; 

448 
val prop = Thm.full_prop_of thm; 

12125
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

449 
val prf' = Proofterm.rewrite_proof_notypes ([], []) prf 
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

450 
in 
17066  451 
ProofContext.pretty_proof ctxt 
452 
(if full then Reconstruct.reconstruct_proof thy prop prf' else prf') 

12125
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

453 
end 
15531  454 
 SOME args => Pretty.chunks 
17066  455 
(map (ProofContext.pretty_proof_of (Proof.context_of state) full) 
19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

456 
(Proof.get_thmss state args))); 
11524
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11017
diff
changeset

457 

19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

458 
fun string_of_prop state s = 
5831  459 
let 
12055  460 
val ctxt = Proof.context_of state; 
461 
val prop = ProofContext.read_prop ctxt s; 

19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

462 
in Pretty.string_of (Pretty.quote (ProofContext.pretty_term ctxt prop)) end; 
5831  463 

19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

464 
fun string_of_term state s = 
5831  465 
let 
12055  466 
val ctxt = Proof.context_of state; 
467 
val t = ProofContext.read_term ctxt s; 

5831  468 
val T = Term.type_of t; 
469 
in 

19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

470 
Pretty.string_of 
12055  471 
(Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.fbrk, 
19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

472 
Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)]) 
9128  473 
end; 
5831  474 

19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

475 
fun string_of_type state s = 
5831  476 
let 
12055  477 
val ctxt = Proof.context_of state; 
478 
val T = ProofContext.read_typ ctxt s; 

19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

479 
in Pretty.string_of (Pretty.quote (ProofContext.pretty_typ ctxt T)) end; 
9128  480 

19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

481 
fun print_item string_of (modes, arg) = Toplevel.keep (fn state => with_modes modes (fn () => 
21003
37492b0062c6
renamed print_lthms to print_facts, do not insist on proof state;
wenzelm
parents:
20978
diff
changeset

482 
writeln (string_of (Toplevel.enter_proof_body state) arg))); 
19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

483 

c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

484 
in 
9128  485 

19268  486 
val print_stmts = print_item string_of_stmts; 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12758
diff
changeset

487 
val print_thms = print_item string_of_thms; 
19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

488 
val print_prfs = print_item o string_of_prfs; 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12758
diff
changeset

489 
val print_prop = print_item string_of_prop; 
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12758
diff
changeset

490 
val print_term = print_item string_of_term; 
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12758
diff
changeset

491 
val print_type = print_item string_of_type; 
5831  492 

19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

493 
end; 
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

494 

12938
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

495 

a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

496 
(* markup commands *) 
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

497 

a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

498 
fun add_header s = Toplevel.keep' (fn int => fn state => 
17262
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

499 
(Toplevel.assert (Toplevel.is_toplevel state); 
19057  500 
if int then OuterSyntax.check_text s NONE else ())); 
12938
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

501 

12953
7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

502 
local 
7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

503 

19057  504 
fun present _ txt true node = OuterSyntax.check_text txt (SOME node) 
505 
 present f (s, _) false node = 

20957  506 
Context.setmp (try (Toplevel.cases_node Context.theory_of Proof.theory_of) node) f s; 
12953
7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

507 

19057  508 
fun present_local_theory f (loc, txt) = Toplevel.present_local_theory loc (present f txt); 
509 
fun present_proof f txt = Toplevel.print o Toplevel.present_proof (present f txt); 

12938
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

510 

12953
7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

511 
in 
7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

512 

19057  513 
val add_chapter = present_local_theory Present.section; 
514 
val add_section = present_local_theory Present.section; 

515 
val add_subsection = present_local_theory Present.subsection; 

516 
val add_subsubsection = present_local_theory Present.subsubsection; 

517 
val add_text = present_local_theory (K ()); 

518 
fun add_text_raw txt = present_local_theory (K ()) (NONE, txt); 

519 
val add_txt = present_proof (K ()); 

520 
val add_txt_raw = add_txt; 

521 
val add_sect = add_txt; 

522 
val add_subsect = add_txt; 

523 
val add_subsubsect = add_txt; 

12938
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

524 

5831  525 
end; 
12953
7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

526 

7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

527 
end; 