author  berghofe 
Mon, 03 Feb 2003 11:07:09 +0100  
changeset 13801  6c5c5bdfae84 
parent 13284  20c818c966e6 
child 14934  bf9f525d4821 
permissions  rwrr 
5831  1 
(* Title: Pure/Isar/isar_cmd.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

8807  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
5831  5 

6 
Nonlogical toplevel commands. 

7 
*) 

8 

9 
signature ISAR_CMD = 

10 
sig 

7462  11 
val welcome: Toplevel.transition > Toplevel.transition 
12 
val init_toplevel: Toplevel.transition > Toplevel.transition 

5831  13 
val exit: Toplevel.transition > Toplevel.transition 
14 
val quit: Toplevel.transition > Toplevel.transition 

7908  15 
val touch_child_thys: string > Toplevel.transition > Toplevel.transition 
7101  16 
val touch_all_thys: Toplevel.transition > Toplevel.transition 
17 
val touch_thy: string > Toplevel.transition > Toplevel.transition 

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

7931  19 
val kill_thy: string > Toplevel.transition > Toplevel.transition 
9731  20 
val pr: string list * (int option * int option) > Toplevel.transition > Toplevel.transition 
8453  21 
val disable_pr: Toplevel.transition > Toplevel.transition 
22 
val enable_pr: Toplevel.transition > Toplevel.transition 

6734  23 
val cannot_undo: string > Toplevel.transition > Toplevel.transition 
7729  24 
val clear_undos_theory: int > Toplevel.transition > Toplevel.transition 
6742  25 
val redo: Toplevel.transition > Toplevel.transition 
26 
val undos_proof: int > Toplevel.transition > Toplevel.transition 

7936  27 
val kill_proof_notify: (unit > unit) > Toplevel.transition > Toplevel.transition 
6742  28 
val kill_proof: Toplevel.transition > Toplevel.transition 
29 
val undo_theory: Toplevel.transition > Toplevel.transition 

6686  30 
val undo: Toplevel.transition > Toplevel.transition 
8498  31 
val kill: Toplevel.transition > Toplevel.transition 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12758
diff
changeset

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

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

34 
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

35 
val use_mltext: bool > string > Toplevel.transition > Toplevel.transition 
5831  36 
val use_commit: Toplevel.transition > Toplevel.transition 
37 
val cd: string > Toplevel.transition > Toplevel.transition 

38 
val pwd: Toplevel.transition > Toplevel.transition 

39 
val use_thy: string > Toplevel.transition > Toplevel.transition 

6694  40 
val use_thy_only: string > Toplevel.transition > Toplevel.transition 
6195  41 
val update_thy: string > Toplevel.transition > Toplevel.transition 
7101  42 
val update_thy_only: string > Toplevel.transition > Toplevel.transition 
7124  43 
val pretty_setmargin: int > Toplevel.transition > Toplevel.transition 
7308  44 
val print_context: Toplevel.transition > Toplevel.transition 
5831  45 
val print_theory: Toplevel.transition > Toplevel.transition 
46 
val print_syntax: Toplevel.transition > Toplevel.transition 

5880  47 
val print_theorems: Toplevel.transition > Toplevel.transition 
12060  48 
val print_locales: Toplevel.transition > Toplevel.transition 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12758
diff
changeset

49 
val print_locale: Locale.expr * Args.src Locale.element list 
12758  50 
> Toplevel.transition > Toplevel.transition 
5831  51 
val print_attributes: Toplevel.transition > Toplevel.transition 
12382  52 
val print_rules: Toplevel.transition > Toplevel.transition 
11666  53 
val print_induct_rules: Toplevel.transition > Toplevel.transition 
9219  54 
val print_trans_rules: Toplevel.transition > Toplevel.transition 
5831  55 
val print_methods: Toplevel.transition > Toplevel.transition 
9219  56 
val print_antiquotations: Toplevel.transition > Toplevel.transition 
13284  57 
val print_thms_containing: int option * string list 
58 
> Toplevel.transition > Toplevel.transition 

9454  59 
val thm_deps: (string * Args.src list) list > Toplevel.transition > Toplevel.transition 
5831  60 
val print_binds: Toplevel.transition > Toplevel.transition 
61 
val print_lthms: Toplevel.transition > Toplevel.transition 

8369  62 
val print_cases: Toplevel.transition > Toplevel.transition 
13801
6c5c5bdfae84
Moved print_intros from proof_general.ML to Isar/isar_cmd.ML
berghofe
parents:
13284
diff
changeset

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

64 
val print_thms: string list * (string * Args.src list) list 
10581  65 
> Toplevel.transition > Toplevel.transition 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12758
diff
changeset

66 
val print_prfs: bool > string list * (string * Args.src list) list option 
11524
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11017
diff
changeset

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

68 
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

69 
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

70 
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

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

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

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

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

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

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

77 
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

78 
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

79 
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

80 
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

81 
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

82 
val add_txt_raw: string * Position.T > Toplevel.transition > Toplevel.transition 
5831  83 
end; 
84 

85 
structure IsarCmd: ISAR_CMD = 

86 
struct 

87 

88 

7462  89 
(* variations on init / exit *) 
90 

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

92 
val welcome = Toplevel.imperative (writeln o Session.welcome); 

5831  93 

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

95 
(Context.set_context (try Toplevel.theory_of state); 

6635  96 
writeln "Leaving the Isar loop. Invoke 'loop();' to restart."; 
5831  97 
raise Toplevel.TERMINATE)); 
98 

99 
val quit = Toplevel.imperative quit; 

100 

7101  101 

102 
(* touch theories *) 

103 

7908  104 
fun touch_child_thys name = Toplevel.imperative (fn () => ThyInfo.touch_child_thys name); 
7101  105 
val touch_all_thys = Toplevel.imperative ThyInfo.touch_all_thys; 
106 
fun touch_thy name = Toplevel.imperative (fn () => ThyInfo.touch_thy name); 

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

7931  108 
fun kill_thy name = Toplevel.imperative (fn () => IsarThy.kill_theory name); 
7101  109 

5831  110 

8453  111 
(* print state *) 
112 

8463  113 
fun with_modes modes e = 
114 
Library.setmp print_mode (modes @ ! print_mode) e (); 

115 

9731  116 
fun set_limit _ None = () 
117 
 set_limit r (Some n) = r := n; 

118 

119 
fun pr (ms, (lim1, lim2)) = Toplevel.keep (fn state => 

120 
(set_limit goals_limit lim1; set_limit ProofContext.prems_limit lim2; Toplevel.quiet := false; 

8886  121 
with_modes ms (fn () => Toplevel.print_state true state))); 
8453  122 

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

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

125 

126 

6686  127 
(* history commands *) 
128 

6734  129 
fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt)); 
7729  130 
val clear_undos_theory = Toplevel.history o History.clear; 
6686  131 
val redo = Toplevel.history History.redo o Toplevel.proof ProofHistory.redo; 
132 

6742  133 
fun undos_proof n = Toplevel.proof (fn prf => 
134 
if ProofHistory.is_initial prf then raise Toplevel.UNDEF else funpow n ProofHistory.undo prf); 

6686  135 

7936  136 
fun kill_proof_notify (f: unit > unit) = Toplevel.history (fn hist => 
6742  137 
(case History.current hist of 
138 
Toplevel.Theory _ => raise Toplevel.UNDEF 

7936  139 
 Toplevel.Proof _ => (f (); History.undo hist))); 
140 

141 
val kill_proof = kill_proof_notify (K ()); 

6686  142 

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

6686  145 

7413  146 
val undo = Toplevel.kill o undo_theory o undos_proof 1; 
8498  147 
val kill = Toplevel.kill o kill_proof; 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12758
diff
changeset

148 
val back = Toplevel.proof o ProofHistory.back; 
9273  149 

6686  150 

5831  151 
(* use ML text *) 
152 

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

153 
fun use name = Toplevel.keep (fn state => 
6264  154 
Context.setmp (try Toplevel.theory_of state) ThyInfo.use name); 
5831  155 

156 
(*passes changes of theory context*) 

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

157 
val use_mltext_theory = Toplevel.theory' o Context.use_mltext_theory; 
5831  158 

159 
(*ignore result theory context*) 

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

160 
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

161 
(Context.use_mltext txt (v andalso verb) (try Toplevel.theory_of state))); 
5831  162 

163 
(*Note: commit is dynamically bound*) 

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

164 
val use_commit = use_mltext false "commit();"; 
5831  165 

166 

167 
(* current working directory *) 

168 

7790  169 
fun cd dir = Toplevel.imperative (fn () => (File.cd (Path.unpack dir))); 
170 
val pwd = Toplevel.imperative (fn () => writeln (Path.pack (File.pwd ()))); 

5831  171 

172 

173 
(* load theory files *) 

174 

6243  175 
fun use_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy name); 
6694  176 
fun use_thy_only name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy_only name); 
6243  177 
fun update_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.update_thy name); 
7124  178 
fun update_thy_only name = 
179 
Toplevel.imperative (fn () => Context.save ThyInfo.update_thy_only name); 

180 

181 

182 
(* pretty_setmargin *) 

183 

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

5831  185 

186 

9513  187 
(* print parts of theory and proof context *) 
5831  188 

7308  189 
val print_context = Toplevel.keep Toplevel.print_state_context; 
9513  190 

191 
val print_theory = Toplevel.unknown_theory o 

192 
Toplevel.keep (PureThy.print_theory o Toplevel.theory_of); 

193 

194 
val print_syntax = Toplevel.unknown_theory o 

12069  195 
Toplevel.keep (Display.print_syntax o Toplevel.theory_of) o 
196 
Toplevel.keep (ProofContext.print_syntax o Proof.context_of o Toplevel.proof_of); 

9513  197 

198 
val print_theorems = Toplevel.unknown_theory o 

199 
Toplevel.keep (PureThy.print_theorems o Toplevel.theory_of); 

200 

12060  201 
val print_locales = Toplevel.unknown_theory o 
202 
Toplevel.keep (Locale.print_locales o Toplevel.theory_of); 

203 

12758  204 
fun print_locale (import, body) = Toplevel.unknown_theory o Toplevel.keep (fn state => 
205 
let val thy = Toplevel.theory_of state in 

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

206 
Locale.print_locale thy import (map (Locale.attribute (Attrib.local_attribute thy)) body) 
12758  207 
end); 
12060  208 

9513  209 
val print_attributes = Toplevel.unknown_theory o 
210 
Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of); 

211 

12382  212 
val print_rules = Toplevel.unknown_context o 
213 
Toplevel.keep (Toplevel.node_case ContextRules.print_global_rules 

214 
(ContextRules.print_local_rules o Proof.context_of)); 

215 

11666  216 
val print_induct_rules = Toplevel.unknown_context o 
217 
Toplevel.keep (Toplevel.node_case InductAttrib.print_global_rules 

218 
(InductAttrib.print_local_rules o Proof.context_of)); 

219 

9513  220 
val print_trans_rules = Toplevel.unknown_context o 
221 
Toplevel.keep (Toplevel.node_case Calculation.print_global_rules 

222 
(Calculation.print_local_rules o Proof.context_of)); 

223 

224 
val print_methods = Toplevel.unknown_theory o 

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

226 

9219  227 
val print_antiquotations = Toplevel.imperative IsarOutput.print_antiquotations; 
5831  228 

13284  229 
fun print_thms_containing (lim, spec) = Toplevel.unknown_theory o Toplevel.keep (fn state => 
13273  230 
ProofContext.print_thms_containing 
13284  231 
(Toplevel.node_case ProofContext.init Proof.context_of state) lim spec); 
7615  232 

9513  233 
fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state => 
9454  234 
ThmDeps.thm_deps (IsarThy.get_thmss args (Toplevel.enter_forward_proof state))); 
235 

5831  236 

237 
(* print proof context contents *) 

238 

9513  239 
val print_binds = Toplevel.unknown_proof o Toplevel.keep (fn state => 
240 
ProofContext.setmp_verbose 

241 
ProofContext.print_binds (Proof.context_of (Toplevel.proof_of state))); 

242 

243 
val print_lthms = Toplevel.unknown_proof o Toplevel.keep (fn state => 

244 
ProofContext.setmp_verbose 

12055  245 
ProofContext.print_lthms (Proof.context_of (Toplevel.proof_of state))); 
9513  246 

247 
val print_cases = Toplevel.unknown_proof o Toplevel.keep (fn state => 

248 
ProofContext.setmp_verbose 

249 
ProofContext.print_cases (Proof.context_of (Toplevel.proof_of state))); 

5831  250 

13801
6c5c5bdfae84
Moved print_intros from proof_general.ML to Isar/isar_cmd.ML
berghofe
parents:
13284
diff
changeset

251 
val print_intros = Toplevel.unknown_proof o Toplevel.keep (fn state => 
6c5c5bdfae84
Moved print_intros from proof_general.ML to Isar/isar_cmd.ML
berghofe
parents:
13284
diff
changeset

252 
let 
6c5c5bdfae84
Moved print_intros from proof_general.ML to Isar/isar_cmd.ML
berghofe
parents:
13284
diff
changeset

253 
val (ctxt, (_, st)) = Proof.get_goal (Toplevel.proof_of state) 
6c5c5bdfae84
Moved print_intros from proof_general.ML to Isar/isar_cmd.ML
berghofe
parents:
13284
diff
changeset

254 
val prt_fact = ProofContext.pretty_fact ctxt 
6c5c5bdfae84
Moved print_intros from proof_general.ML to Isar/isar_cmd.ML
berghofe
parents:
13284
diff
changeset

255 
val thy = ProofContext.theory_of ctxt 
6c5c5bdfae84
Moved print_intros from proof_general.ML to Isar/isar_cmd.ML
berghofe
parents:
13284
diff
changeset

256 
val facts = map (apsnd single) (PureThy.find_intros_goal thy st 1) 
6c5c5bdfae84
Moved print_intros from proof_general.ML to Isar/isar_cmd.ML
berghofe
parents:
13284
diff
changeset

257 
in map prt_fact (rev facts) > Pretty.chunks > Pretty.writeln end); 
6c5c5bdfae84
Moved print_intros from proof_general.ML to Isar/isar_cmd.ML
berghofe
parents:
13284
diff
changeset

258 

5831  259 

7012  260 
(* print theorems / types / terms / props *) 
5880  261 

9128  262 
fun string_of_thms state ms args = with_modes ms (fn () => 
12055  263 
Pretty.string_of (ProofContext.pretty_thms (Proof.context_of state) 
264 
(IsarThy.get_thmss args state))); 

5895  265 

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

266 
fun string_of_prfs full state ms arg = with_modes ms (fn () => 
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

267 
Pretty.string_of (case arg of (* FIXME context syntax!? *) 
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

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

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

270 
val (_, (_, thm)) = Proof.get_goal state; 
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

271 
val {sign, prop, der = (_, prf), ...} = rep_thm thm; 
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

272 
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

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

274 
ProofSyntax.pretty_proof sign 
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

275 
(if full then Reconstruct.reconstruct_proof sign prop prf' else prf') 
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

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

277 
 Some args => Pretty.chunks 
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

278 
(map (ProofSyntax.pretty_proof_of full) (IsarThy.get_thmss args state)))); 
11524
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11017
diff
changeset

279 

9128  280 
fun string_of_prop state ms s = 
5831  281 
let 
12055  282 
val ctxt = Proof.context_of state; 
283 
val prop = ProofContext.read_prop ctxt s; 

284 
in 

285 
with_modes ms (fn () => Pretty.string_of (Pretty.quote (ProofContext.pretty_term ctxt prop))) 

286 
end; 

5831  287 

9128  288 
fun string_of_term state ms s = 
5831  289 
let 
12055  290 
val ctxt = Proof.context_of state; 
291 
val t = ProofContext.read_term ctxt s; 

5831  292 
val T = Term.type_of t; 
293 
in 

9128  294 
with_modes ms (fn () => Pretty.string_of 
12055  295 
(Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.fbrk, 
296 
Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)])) 

9128  297 
end; 
5831  298 

9128  299 
fun string_of_type state ms s = 
5831  300 
let 
12055  301 
val ctxt = Proof.context_of state; 
302 
val T = ProofContext.read_typ ctxt s; 

303 
in with_modes ms (fn () => Pretty.string_of (Pretty.quote (ProofContext.pretty_typ ctxt T))) end; 

9128  304 

305 
fun print_item string_of (x, y) = Toplevel.keep (fn state => 

9454  306 
writeln (string_of (Toplevel.enter_forward_proof state) x y)); 
9128  307 

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

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

309 
fun print_prfs full = print_item (string_of_prfs full); 
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12758
diff
changeset

310 
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

311 
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

312 
val print_type = print_item string_of_type; 
5831  313 

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

314 

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

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

316 

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

317 
fun add_header s = Toplevel.keep' (fn int => fn state => 
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

318 
(if Toplevel.is_toplevel state then () else raise Toplevel.UNDEF; 
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

319 
OuterSyntax.check_text s int state)); 
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

320 

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

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

322 

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

323 
fun present_text assert_proof present (s, pos) = Toplevel.keep' (fn int => fn state => 
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

324 
(if can Toplevel.proof_of state = assert_proof then () else raise Toplevel.UNDEF; 
12953
7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

325 
Context.setmp (Some (Toplevel.theory_of state)) present s; 
12938
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

326 
OuterSyntax.check_text (s, pos) int state; 
12953
7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

327 
raise Toplevel.UNDEF)); 
7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

328 

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

329 
fun theory f x = Toplevel.theory I o present_text false f x; 
7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

330 
fun proof f x = Toplevel.print o Toplevel.proof (ProofHistory.apply I) o present_text true f x; 
12938
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

331 

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

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

333 

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

334 
val add_chapter = theory Present.section; 
7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

335 
val add_section = theory Present.section; 
7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

336 
val add_subsection = theory Present.subsection; 
7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

337 
val add_subsubsection = theory Present.subsubsection; 
7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

338 
val add_text = theory (K ()); 
12938
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

339 
val add_text_raw = add_text; 
12953
7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

340 
val add_txt = proof (K ()); 
12938
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

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

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

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

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

345 

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

347 

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

348 
end; 