author  wenzelm 
Mon, 05 Sep 2005 17:38:20 +0200  
changeset 17262  63cf42df2723 
parent 17228  19b460b39dad 
child 17352  5bc9f8c81d58 
permissions  rwrr 
5831  1 
(* Title: Pure/Isar/isar_cmd.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

5 
Nonlogical toplevel commands. 

6 
*) 

7 

8 
signature ISAR_CMD = 

9 
sig 

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

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

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

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

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

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

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

6686  29 
val undo: Toplevel.transition > Toplevel.transition 
8498  30 
val kill: Toplevel.transition > Toplevel.transition 
17066  31 
val back: Toplevel.transition > Toplevel.transition 
14950  32 
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

33 
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

34 
val use_mltext: bool > string > Toplevel.transition > Toplevel.transition 
5831  35 
val use_commit: Toplevel.transition > Toplevel.transition 
14950  36 
val cd: Path.T > Toplevel.transition > Toplevel.transition 
5831  37 
val pwd: Toplevel.transition > Toplevel.transition 
38 
val use_thy: string > Toplevel.transition > Toplevel.transition 

6694  39 
val use_thy_only: string > Toplevel.transition > Toplevel.transition 
6195  40 
val update_thy: string > Toplevel.transition > Toplevel.transition 
7101  41 
val update_thy_only: string > Toplevel.transition > Toplevel.transition 
14950  42 
val display_drafts: Path.T list > Toplevel.transition > Toplevel.transition 
43 
val print_drafts: Path.T list > Toplevel.transition > Toplevel.transition 

7124  44 
val pretty_setmargin: int > Toplevel.transition > Toplevel.transition 
7308  45 
val print_context: Toplevel.transition > Toplevel.transition 
5831  46 
val print_theory: Toplevel.transition > Toplevel.transition 
47 
val print_syntax: Toplevel.transition > Toplevel.transition 

5880  48 
val print_theorems: Toplevel.transition > Toplevel.transition 
12060  49 
val print_locales: Toplevel.transition > Toplevel.transition 
17228  50 
val print_locale: bool * (Locale.expr * Locale.element list) 
12758  51 
> Toplevel.transition > Toplevel.transition 
17139
165c97f9bb63
Printing of interpretations: option to show witness theorems;
ballarin
parents:
17066
diff
changeset

52 
val print_registrations: bool > string > Toplevel.transition > Toplevel.transition 
5831  53 
val print_attributes: Toplevel.transition > Toplevel.transition 
16026  54 
val print_simpset: Toplevel.transition > Toplevel.transition 
12382  55 
val print_rules: Toplevel.transition > Toplevel.transition 
11666  56 
val print_induct_rules: Toplevel.transition > Toplevel.transition 
9219  57 
val print_trans_rules: Toplevel.transition > Toplevel.transition 
5831  58 
val print_methods: Toplevel.transition > Toplevel.transition 
9219  59 
val print_antiquotations: Toplevel.transition > Toplevel.transition 
16026  60 
val thm_deps: (thmref * Attrib.src list) list > 
61 
Toplevel.transition > Toplevel.transition 

16037  62 
val find_theorems: int option * (bool * string FindTheorems.criterion) list 
13284  63 
> Toplevel.transition > Toplevel.transition 
5831  64 
val print_binds: Toplevel.transition > Toplevel.transition 
65 
val print_lthms: Toplevel.transition > Toplevel.transition 

8369  66 
val print_cases: Toplevel.transition > Toplevel.transition 
15703  67 
val print_thms: string list * (thmref * Attrib.src list) list 
10581  68 
> Toplevel.transition > Toplevel.transition 
15703  69 
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

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

71 
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

72 
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

73 
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

74 
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

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

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

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

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

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

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

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

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

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

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

85 
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

86 
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

87 
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

88 
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

89 
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

90 
val add_txt_raw: string * Position.T > Toplevel.transition > Toplevel.transition 
5831  91 
end; 
92 

93 
structure IsarCmd: ISAR_CMD = 

94 
struct 

95 

96 

7462  97 
(* variations on init / exit *) 
98 

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

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

5831  101 

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

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

6635  104 
writeln "Leaving the Isar loop. Invoke 'loop();' to restart."; 
5831  105 
raise Toplevel.TERMINATE)); 
106 

107 
val quit = Toplevel.imperative quit; 

108 

7101  109 

110 
(* touch theories *) 

111 

7908  112 
fun touch_child_thys name = Toplevel.imperative (fn () => ThyInfo.touch_child_thys name); 
7101  113 
val touch_all_thys = Toplevel.imperative ThyInfo.touch_all_thys; 
114 
fun touch_thy name = Toplevel.imperative (fn () => ThyInfo.touch_thy name); 

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

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

5831  118 

8453  119 
(* print state *) 
120 

8463  121 
fun with_modes modes e = 
122 
Library.setmp print_mode (modes @ ! print_mode) e (); 

123 

15531  124 
fun set_limit _ NONE = () 
125 
 set_limit r (SOME n) = r := n; 

9731  126 

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

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

8886  129 
with_modes ms (fn () => Toplevel.print_state true state))); 
8453  130 

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

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

133 

134 

6686  135 
(* history commands *) 
136 

6734  137 
fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt)); 
7729  138 
val clear_undos_theory = Toplevel.history o History.clear; 
16812  139 

140 
val redo = 

141 
Toplevel.history History.redo o 

142 
Toplevel.actual_proof ProofHistory.redo o 

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

143 
Toplevel.skip_proof History.redo; 
6686  144 

16812  145 
fun undos_proof n = 
146 
Toplevel.actual_proof (fn prf => 

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

147 
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

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

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

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

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

154 
 _ => (f (); History.undo hist))); 
7936  155 

156 
val kill_proof = kill_proof_notify (K ()); 

6686  157 

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

6686  160 

7413  161 
val undo = Toplevel.kill o undo_theory o undos_proof 1; 
8498  162 
val kill = Toplevel.kill o kill_proof; 
17066  163 
val back = Toplevel.proof ProofHistory.back; 
9273  164 

6686  165 

5831  166 
(* use ML text *) 
167 

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

5831  170 

171 
(*passes changes of theory context*) 

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

172 
val use_mltext_theory = Toplevel.theory' o Context.use_mltext_theory; 
5831  173 

174 
(*ignore result theory context*) 

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

175 
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

176 
(Context.use_mltext txt (v andalso verb) (try Toplevel.theory_of state))); 
5831  177 

16193  178 
(*commit is dynamically bound!*) 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12758
diff
changeset

179 
val use_commit = use_mltext false "commit();"; 
5831  180 

181 

182 
(* current working directory *) 

183 

14950  184 
fun cd path = Toplevel.imperative (fn () => (File.cd path)); 
7790  185 
val pwd = Toplevel.imperative (fn () => writeln (Path.pack (File.pwd ()))); 
5831  186 

187 

188 
(* load theory files *) 

189 

6243  190 
fun use_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy name); 
6694  191 
fun use_thy_only name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy_only name); 
6243  192 
fun update_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.update_thy name); 
7124  193 
fun update_thy_only name = 
194 
Toplevel.imperative (fn () => Context.save ThyInfo.update_thy_only name); 

195 

196 

14934  197 
(* present draft files *) 
198 

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

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

14934  202 

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

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

14934  206 

207 

7124  208 
(* pretty_setmargin *) 
209 

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

5831  211 

212 

9513  213 
(* print parts of theory and proof context *) 
5831  214 

7308  215 
val print_context = Toplevel.keep Toplevel.print_state_context; 
9513  216 

217 
val print_theory = Toplevel.unknown_theory o 

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

219 

220 
val print_syntax = Toplevel.unknown_theory o 

12069  221 
Toplevel.keep (Display.print_syntax o Toplevel.theory_of) o 
222 
Toplevel.keep (ProofContext.print_syntax o Proof.context_of o Toplevel.proof_of); 

9513  223 

17066  224 
val print_theorems_proof = Toplevel.keep (fn state => 
225 
ProofContext.setmp_verbose 

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

227 

16499
2076b2e6ac58
print_theorems: proper use of PureThy.print_theorems_diff;
wenzelm
parents:
16258
diff
changeset

228 
val print_theorems = Toplevel.unknown_theory o Toplevel.keep (fn state => 
2076b2e6ac58
print_theorems: proper use of PureThy.print_theorems_diff;
wenzelm
parents:
16258
diff
changeset

229 
(case History.previous (Toplevel.node_history_of state) of 
17066  230 
SOME (Toplevel.Theory (prev_thy, _)) => PureThy.print_theorems_diff prev_thy 
231 
 _ => PureThy.print_theorems) (Toplevel.theory_of state)) o print_theorems_proof; 

9513  232 

12060  233 
val print_locales = Toplevel.unknown_theory o 
234 
Toplevel.keep (Locale.print_locales o Toplevel.theory_of); 

235 

17228  236 
fun print_locale (show_facts, (import, body)) = Toplevel.unknown_theory o Toplevel.keep (fn state => 
237 
Locale.print_locale (Toplevel.theory_of state) show_facts import body); 

15596  238 

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

239 
fun print_registrations show_wits name = Toplevel.unknown_context o 
165c97f9bb63
Printing of interpretations: option to show witness theorems;
ballarin
parents:
17066
diff
changeset

240 
Toplevel.keep (Toplevel.node_case (Locale.print_global_registrations show_wits name) 
165c97f9bb63
Printing of interpretations: option to show witness theorems;
ballarin
parents:
17066
diff
changeset

241 
(Locale.print_local_registrations show_wits name o Proof.context_of)); 
12060  242 

9513  243 
val print_attributes = Toplevel.unknown_theory o 
244 
Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of); 

245 

16026  246 
val print_simpset = Toplevel.unknown_context o 
247 
Toplevel.keep (Toplevel.node_case Simplifier.print_simpset 

248 
(Simplifier.print_local_simpset o Proof.context_of)); 

249 

12382  250 
val print_rules = Toplevel.unknown_context o 
251 
Toplevel.keep (Toplevel.node_case ContextRules.print_global_rules 

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

253 

11666  254 
val print_induct_rules = Toplevel.unknown_context o 
255 
Toplevel.keep (Toplevel.node_case InductAttrib.print_global_rules 

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

257 

9513  258 
val print_trans_rules = Toplevel.unknown_context o 
259 
Toplevel.keep (Toplevel.node_case Calculation.print_global_rules 

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

261 

262 
val print_methods = Toplevel.unknown_theory o 

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

264 

9219  265 
val print_antiquotations = Toplevel.imperative IsarOutput.print_antiquotations; 
5831  266 

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

267 

16026  268 
(* retrieve theorems *) 
7615  269 

9513  270 
fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state => 
9454  271 
ThmDeps.thm_deps (IsarThy.get_thmss args (Toplevel.enter_forward_proof state))); 
272 

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

275 
val proof_state = Toplevel.enter_forward_proof state; 

276 
val ctxt = Proof.context_of proof_state; 

277 
val opt_goal = try Proof.get_goal proof_state > Option.map (Thm.prop_of o #2 o #2); 

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

279 

5831  280 

281 
(* print proof context contents *) 

282 

9513  283 
val print_binds = Toplevel.unknown_proof o Toplevel.keep (fn state => 
284 
ProofContext.setmp_verbose 

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

286 

17066  287 
val print_lthms = Toplevel.unknown_proof o print_theorems_proof; 
9513  288 

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

290 
ProofContext.setmp_verbose 

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

5831  292 

293 

7012  294 
(* print theorems / types / terms / props *) 
5880  295 

9128  296 
fun string_of_thms state ms args = with_modes ms (fn () => 
12055  297 
Pretty.string_of (ProofContext.pretty_thms (Proof.context_of state) 
298 
(IsarThy.get_thmss args state))); 

5895  299 

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

300 
fun string_of_prfs full state ms arg = with_modes ms (fn () => 
17066  301 
Pretty.string_of (case arg of 
15531  302 
NONE => 
12125
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

303 
let 
17066  304 
val (ctxt, (_, thm)) = Proof.get_goal state; 
305 
val {thy, der = (_, prf), ...} = Thm.rep_thm thm; 

306 
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

307 
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

308 
in 
17066  309 
ProofContext.pretty_proof ctxt 
310 
(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

311 
end 
15531  312 
 SOME args => Pretty.chunks 
17066  313 
(map (ProofContext.pretty_proof_of (Proof.context_of state) full) 
314 
(IsarThy.get_thmss args state)))); 

11524
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11017
diff
changeset

315 

9128  316 
fun string_of_prop state ms s = 
5831  317 
let 
12055  318 
val ctxt = Proof.context_of state; 
319 
val prop = ProofContext.read_prop ctxt s; 

320 
in 

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

322 
end; 

5831  323 

9128  324 
fun string_of_term state ms s = 
5831  325 
let 
12055  326 
val ctxt = Proof.context_of state; 
327 
val t = ProofContext.read_term ctxt s; 

5831  328 
val T = Term.type_of t; 
329 
in 

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

9128  333 
end; 
5831  334 

9128  335 
fun string_of_type state ms s = 
5831  336 
let 
12055  337 
val ctxt = Proof.context_of state; 
338 
val T = ProofContext.read_typ ctxt s; 

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

9128  340 

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

9454  342 
writeln (string_of (Toplevel.enter_forward_proof state) x y)); 
9128  343 

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

344 
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

345 
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

346 
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

347 
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

348 
val print_type = print_item string_of_type; 
5831  349 

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

350 

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

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

352 

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

353 
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

354 
(Toplevel.assert (Toplevel.is_toplevel state); 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

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

356 

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

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

358 

17262
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

359 
fun enter_locale NONE = Toplevel.theory I 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

360 
 enter_locale (SOME loc) = Toplevel.theory_context (fn thy => 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

361 
(thy, #3 (Locale.read_context_statement (SOME loc) [] [] (ProofContext.init thy)))); 
12953
7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

362 

17262
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

363 
fun present_text proof present loc (s, pos) = Toplevel.keep' (fn int => fn state => 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

364 
(Toplevel.assert (can Toplevel.proof_of state = proof); 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

365 
if int then 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

366 
state 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

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

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

369 
(Toplevel.empty > Toplevel.position pos > enter_locale loc > Toplevel.keep (K ())) 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

370 
> OuterSyntax.check_text (s, pos) 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

371 
else Context.setmp (SOME (Toplevel.theory_of state)) present s; 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

372 
raise Toplevel.UNDEF)); 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

373 

63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

374 
fun theory f (loc, txt) = enter_locale loc o present_text false f loc txt; 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

375 
fun proof f txt = 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

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

377 

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

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

379 

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

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

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

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

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

384 
val add_text = theory (K ()); 
17262
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

385 
fun add_text_raw txt = theory (K ()) (NONE, txt); 
12953
7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

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

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

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

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

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

391 

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

393 

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

394 
end; 