9 struct |
9 struct |
10 |
10 |
11 structure P = OuterParse and K = OuterKeyword; |
11 structure P = OuterParse and K = OuterKeyword; |
12 |
12 |
13 |
13 |
|
14 (** keywords **) |
|
15 |
|
16 (*keep keywords consistent with the parsers, otherwise be prepared for |
|
17 unexpected errors*) |
|
18 |
|
19 val _ = OuterSyntax.keywords |
|
20 ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=", |
|
21 "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>", |
|
22 "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]", |
|
23 "advanced", "and", "assumes", "attach", "begin", "binder", "concl", |
|
24 "constrains", "defines", "fixes", "for", "identifier", "if", |
|
25 "imports", "in", "includes", "infix", "infixl", "infixr", "is", |
|
26 "local_syntax", "notes", "obtains", "open", "output", "overloaded", "shows", |
|
27 "structure", "unchecked", "uses", "where", "|"]; |
|
28 |
|
29 |
14 (** init and exit **) |
30 (** init and exit **) |
15 |
31 |
16 val theoryP = |
32 val _ = |
17 OuterSyntax.command "theory" "begin theory" (K.tag_theory K.thy_begin) |
33 OuterSyntax.command "theory" "begin theory" (K.tag_theory K.thy_begin) |
18 (ThyHeader.args >> (Toplevel.print oo IsarCmd.theory)); |
34 (ThyHeader.args >> (Toplevel.print oo IsarCmd.theory)); |
19 |
35 |
20 val endP = |
36 val _ = |
21 OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end) |
37 OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end) |
22 (Scan.succeed (Toplevel.exit o Toplevel.end_local_theory)); |
38 (Scan.succeed (Toplevel.exit o Toplevel.end_local_theory)); |
23 |
39 |
24 |
40 |
25 (** markup commands **) |
41 (** markup commands **) |
26 |
42 |
27 val headerP = OuterSyntax.markup_command ThyOutput.Markup "header" "theory header" K.diag |
43 val _ = OuterSyntax.markup_command ThyOutput.Markup "header" "theory header" K.diag |
28 (P.position P.text >> IsarCmd.add_header); |
44 (P.position P.text >> IsarCmd.add_header); |
29 |
45 |
30 val chapterP = OuterSyntax.markup_command ThyOutput.Markup "chapter" "chapter heading" |
46 val _ = OuterSyntax.markup_command ThyOutput.Markup "chapter" "chapter heading" |
31 K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_chapter); |
47 K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_chapter); |
32 |
48 |
33 val sectionP = OuterSyntax.markup_command ThyOutput.Markup "section" "section heading" |
49 val _ = OuterSyntax.markup_command ThyOutput.Markup "section" "section heading" |
34 K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_section); |
50 K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_section); |
35 |
51 |
36 val subsectionP = OuterSyntax.markup_command ThyOutput.Markup "subsection" "subsection heading" |
52 val _ = OuterSyntax.markup_command ThyOutput.Markup "subsection" "subsection heading" |
37 K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_subsection); |
53 K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_subsection); |
38 |
54 |
39 val subsubsectionP = |
55 val _ = |
40 OuterSyntax.markup_command ThyOutput.Markup "subsubsection" "subsubsection heading" |
56 OuterSyntax.markup_command ThyOutput.Markup "subsubsection" "subsubsection heading" |
41 K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_subsubsection); |
57 K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_subsubsection); |
42 |
58 |
43 val textP = OuterSyntax.markup_command ThyOutput.MarkupEnv "text" "formal comment (theory)" |
59 val _ = OuterSyntax.markup_command ThyOutput.MarkupEnv "text" "formal comment (theory)" |
44 K.thy_decl (P.opt_target -- P.position P.text >> IsarCmd.add_text); |
60 K.thy_decl (P.opt_target -- P.position P.text >> IsarCmd.add_text); |
45 |
61 |
46 val text_rawP = OuterSyntax.markup_command ThyOutput.Verbatim "text_raw" |
62 val _ = OuterSyntax.markup_command ThyOutput.Verbatim "text_raw" |
47 "raw document preparation text" |
63 "raw document preparation text" |
48 K.thy_decl (P.position P.text >> IsarCmd.add_text_raw); |
64 K.thy_decl (P.position P.text >> IsarCmd.add_text_raw); |
49 |
65 |
50 val sectP = OuterSyntax.markup_command ThyOutput.Markup "sect" "formal comment (proof)" |
66 val _ = OuterSyntax.markup_command ThyOutput.Markup "sect" "formal comment (proof)" |
51 (K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.add_sect); |
67 (K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.add_sect); |
52 |
68 |
53 val subsectP = OuterSyntax.markup_command ThyOutput.Markup "subsect" "formal comment (proof)" |
69 val _ = OuterSyntax.markup_command ThyOutput.Markup "subsect" "formal comment (proof)" |
54 (K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.add_subsect); |
70 (K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.add_subsect); |
55 |
71 |
56 val subsubsectP = OuterSyntax.markup_command ThyOutput.Markup "subsubsect" |
72 val _ = OuterSyntax.markup_command ThyOutput.Markup "subsubsect" |
57 "formal comment (proof)" (K.tag_proof K.prf_heading) |
73 "formal comment (proof)" (K.tag_proof K.prf_heading) |
58 (P.position P.text >> IsarCmd.add_subsubsect); |
74 (P.position P.text >> IsarCmd.add_subsubsect); |
59 |
75 |
60 val txtP = OuterSyntax.markup_command ThyOutput.MarkupEnv "txt" "formal comment (proof)" |
76 val _ = OuterSyntax.markup_command ThyOutput.MarkupEnv "txt" "formal comment (proof)" |
61 (K.tag_proof K.prf_decl) (P.position P.text >> IsarCmd.add_txt); |
77 (K.tag_proof K.prf_decl) (P.position P.text >> IsarCmd.add_txt); |
62 |
78 |
63 val txt_rawP = OuterSyntax.markup_command ThyOutput.Verbatim "txt_raw" |
79 val _ = OuterSyntax.markup_command ThyOutput.Verbatim "txt_raw" |
64 "raw document preparation text (proof)" (K.tag_proof K.prf_decl) |
80 "raw document preparation text (proof)" (K.tag_proof K.prf_decl) |
65 (P.position P.text >> IsarCmd.add_txt_raw); |
81 (P.position P.text >> IsarCmd.add_txt_raw); |
66 |
82 |
67 |
83 |
68 |
84 |
69 (** theory sections **) |
85 (** theory sections **) |
70 |
86 |
71 (* classes and sorts *) |
87 (* classes and sorts *) |
72 |
88 |
73 val classesP = |
89 val _ = |
74 OuterSyntax.command "classes" "declare type classes" K.thy_decl |
90 OuterSyntax.command "classes" "declare type classes" K.thy_decl |
75 (Scan.repeat1 (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- |
91 (Scan.repeat1 (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- |
76 P.!!! (P.list1 P.xname)) []) >> (Toplevel.theory o fold AxClass.axiomatize_class)); |
92 P.!!! (P.list1 P.xname)) []) >> (Toplevel.theory o fold AxClass.axiomatize_class)); |
77 |
93 |
78 val classrelP = |
94 val _ = |
79 OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl |
95 OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl |
80 (P.and_list1 (P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)) |
96 (P.and_list1 (P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)) |
81 >> (Toplevel.theory o AxClass.axiomatize_classrel)); |
97 >> (Toplevel.theory o AxClass.axiomatize_classrel)); |
82 |
98 |
83 val defaultsortP = |
99 val _ = |
84 OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl |
100 OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl |
85 (P.sort >> (Toplevel.theory o Sign.add_defsort)); |
101 (P.sort >> (Toplevel.theory o Sign.add_defsort)); |
86 |
102 |
87 val axclassP = |
103 val _ = |
88 OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl |
104 OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl |
89 (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- |
105 (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- |
90 P.!!! (P.list1 P.xname)) [] |
106 P.!!! (P.list1 P.xname)) [] |
91 -- Scan.repeat (SpecParse.thm_name ":" -- (P.prop >> single)) |
107 -- Scan.repeat (SpecParse.thm_name ":" -- (P.prop >> single)) |
92 >> (fn (x, y) => Toplevel.theory (snd o Class.axclass_cmd x y))); |
108 >> (fn (x, y) => Toplevel.theory (snd o Class.axclass_cmd x y))); |
93 |
109 |
94 |
110 |
95 (* types *) |
111 (* types *) |
96 |
112 |
97 val typedeclP = |
113 val _ = |
98 OuterSyntax.command "typedecl" "type declaration" K.thy_decl |
114 OuterSyntax.command "typedecl" "type declaration" K.thy_decl |
99 (P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) => |
115 (P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) => |
100 Toplevel.theory (Sign.add_typedecls [(a, args, mx)]))); |
116 Toplevel.theory (Sign.add_typedecls [(a, args, mx)]))); |
101 |
117 |
102 val typeabbrP = |
118 val _ = |
103 OuterSyntax.command "types" "declare type abbreviations" K.thy_decl |
119 OuterSyntax.command "types" "declare type abbreviations" K.thy_decl |
104 (Scan.repeat1 |
120 (Scan.repeat1 |
105 (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix'))) |
121 (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix'))) |
106 >> (Toplevel.theory o Sign.add_tyabbrs o |
122 >> (Toplevel.theory o Sign.add_tyabbrs o |
107 map (fn ((args, a), (T, mx)) => (a, args, T, mx)))); |
123 map (fn ((args, a), (T, mx)) => (a, args, T, mx)))); |
108 |
124 |
109 val nontermP = |
125 val _ = |
110 OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols" |
126 OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols" |
111 K.thy_decl (Scan.repeat1 P.name >> (Toplevel.theory o Sign.add_nonterminals)); |
127 K.thy_decl (Scan.repeat1 P.name >> (Toplevel.theory o Sign.add_nonterminals)); |
112 |
128 |
113 val aritiesP = |
129 val _ = |
114 OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl |
130 OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl |
115 (Scan.repeat1 P.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity)); |
131 (Scan.repeat1 P.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity)); |
116 |
132 |
117 |
133 |
118 (* consts and syntax *) |
134 (* consts and syntax *) |
119 |
135 |
120 val judgmentP = |
136 val _ = |
121 OuterSyntax.command "judgment" "declare object-logic judgment" K.thy_decl |
137 OuterSyntax.command "judgment" "declare object-logic judgment" K.thy_decl |
122 (P.const >> (Toplevel.theory o ObjectLogic.add_judgment)); |
138 (P.const >> (Toplevel.theory o ObjectLogic.add_judgment)); |
123 |
139 |
124 val constsP = |
140 val _ = |
125 OuterSyntax.command "consts" "declare constants" K.thy_decl |
141 OuterSyntax.command "consts" "declare constants" K.thy_decl |
126 (Scan.repeat1 P.const >> (Toplevel.theory o Sign.add_consts)); |
142 (Scan.repeat1 P.const >> (Toplevel.theory o Sign.add_consts)); |
127 |
143 |
128 val opt_overloaded = P.opt_keyword "overloaded"; |
144 val opt_overloaded = P.opt_keyword "overloaded"; |
129 |
145 |
130 val finalconstsP = |
146 val _ = |
131 OuterSyntax.command "finalconsts" "declare constants as final" K.thy_decl |
147 OuterSyntax.command "finalconsts" "declare constants as final" K.thy_decl |
132 (opt_overloaded -- Scan.repeat1 P.term >> (uncurry (Toplevel.theory oo Theory.add_finals))); |
148 (opt_overloaded -- Scan.repeat1 P.term >> (uncurry (Toplevel.theory oo Theory.add_finals))); |
133 |
149 |
134 val mode_spec = |
150 val mode_spec = |
135 (P.$$$ "output" >> K ("", false)) || P.name -- Scan.optional (P.$$$ "output" >> K false) true; |
151 (P.$$$ "output" >> K ("", false)) || P.name -- Scan.optional (P.$$$ "output" >> K false) true; |
136 |
152 |
137 val opt_mode = |
153 val opt_mode = |
138 Scan.optional (P.$$$ "(" |-- P.!!! (mode_spec --| P.$$$ ")")) Syntax.default_mode; |
154 Scan.optional (P.$$$ "(" |-- P.!!! (mode_spec --| P.$$$ ")")) Syntax.default_mode; |
139 |
155 |
140 val syntaxP = |
156 val _ = |
141 OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl |
157 OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl |
142 (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Sign.add_modesyntax)); |
158 (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Sign.add_modesyntax)); |
143 |
159 |
144 val no_syntaxP = |
160 val _ = |
145 OuterSyntax.command "no_syntax" "delete syntax declarations" K.thy_decl |
161 OuterSyntax.command "no_syntax" "delete syntax declarations" K.thy_decl |
146 (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Sign.del_modesyntax)); |
162 (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Sign.del_modesyntax)); |
147 |
163 |
148 |
164 |
149 (* translations *) |
165 (* translations *) |
246 (* theorems *) |
262 (* theorems *) |
247 |
263 |
248 fun theorems kind = P.opt_target -- SpecParse.name_facts |
264 fun theorems kind = P.opt_target -- SpecParse.name_facts |
249 >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.theorems kind args)); |
265 >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.theorems kind args)); |
250 |
266 |
251 val theoremsP = |
267 val _ = |
252 OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK); |
268 OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK); |
253 |
269 |
254 val lemmasP = |
270 val _ = |
255 OuterSyntax.command "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK); |
271 OuterSyntax.command "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK); |
256 |
272 |
257 val declareP = |
273 val _ = |
258 OuterSyntax.command "declare" "declare theorems (improper)" K.thy_decl |
274 OuterSyntax.command "declare" "declare theorems (improper)" K.thy_decl |
259 (P.opt_target -- (P.and_list1 SpecParse.xthms1 >> flat) |
275 (P.opt_target -- (P.and_list1 SpecParse.xthms1 >> flat) |
260 >> (fn (loc, args) => Toplevel.local_theory loc |
276 >> (fn (loc, args) => Toplevel.local_theory loc |
261 (#2 o Specification.theorems "" [(("", []), args)]))); |
277 (#2 o Specification.theorems "" [(("", []), args)]))); |
262 |
278 |
263 |
279 |
264 (* name space entry path *) |
280 (* name space entry path *) |
265 |
281 |
266 val globalP = |
282 val _ = |
267 OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl |
283 OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl |
268 (Scan.succeed (Toplevel.theory Sign.root_path)); |
284 (Scan.succeed (Toplevel.theory Sign.root_path)); |
269 |
285 |
270 val localP = |
286 val _ = |
271 OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl |
287 OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl |
272 (Scan.succeed (Toplevel.theory Sign.local_path)); |
288 (Scan.succeed (Toplevel.theory Sign.local_path)); |
273 |
289 |
274 val hideP = |
290 val _ = |
275 OuterSyntax.command "hide" "hide names from given name space" K.thy_decl |
291 OuterSyntax.command "hide" "hide names from given name space" K.thy_decl |
276 ((P.opt_keyword "open" >> not) -- (P.name -- Scan.repeat1 P.xname) >> |
292 ((P.opt_keyword "open" >> not) -- (P.name -- Scan.repeat1 P.xname) >> |
277 (Toplevel.theory o uncurry Sign.hide_names)); |
293 (Toplevel.theory o uncurry Sign.hide_names)); |
278 |
294 |
279 |
295 |
280 (* use ML text *) |
296 (* use ML text *) |
281 |
297 |
282 val useP = |
298 val _ = |
283 OuterSyntax.command "use" "eval ML text from file" (K.tag_ml K.diag) |
299 OuterSyntax.command "use" "eval ML text from file" (K.tag_ml K.diag) |
284 (P.path >> (Toplevel.no_timing oo IsarCmd.use)); |
300 (P.path >> (Toplevel.no_timing oo IsarCmd.use)); |
285 |
301 |
286 val mlP = |
302 val _ = |
287 OuterSyntax.command "ML" "eval ML text (diagnostic)" (K.tag_ml K.diag) |
303 OuterSyntax.command "ML" "eval ML text (diagnostic)" (K.tag_ml K.diag) |
288 (P.text >> IsarCmd.use_mltext true); |
304 (P.text >> IsarCmd.use_mltext true); |
289 |
305 |
290 val ml_commandP = |
306 val _ = |
291 OuterSyntax.command "ML_command" "eval ML text" (K.tag_ml K.diag) |
307 OuterSyntax.command "ML_command" "eval ML text" (K.tag_ml K.diag) |
292 (P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false)); |
308 (P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false)); |
293 |
309 |
294 val ml_setupP = |
310 val _ = |
295 OuterSyntax.command "ML_setup" "eval ML text (may change theory)" (K.tag_ml K.thy_decl) |
311 OuterSyntax.command "ML_setup" "eval ML text (may change theory)" (K.tag_ml K.thy_decl) |
296 (P.text >> IsarCmd.use_mltext_theory); |
312 (P.text >> IsarCmd.use_mltext_theory); |
297 |
313 |
298 val setupP = |
314 val _ = |
299 OuterSyntax.command "setup" "apply ML theory setup" (K.tag_ml K.thy_decl) |
315 OuterSyntax.command "setup" "apply ML theory setup" (K.tag_ml K.thy_decl) |
300 (Scan.option P.text >> (Toplevel.theory o IsarCmd.generic_setup)); |
316 (Scan.option P.text >> (Toplevel.theory o IsarCmd.generic_setup)); |
301 |
317 |
302 val method_setupP = |
318 val _ = |
303 OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl) |
319 OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl) |
304 (((P.name -- P.!!! (P.$$$ "=" |-- P.text -- P.text) >> P.triple2)) |
320 (((P.name -- P.!!! (P.$$$ "=" |-- P.text -- P.text) >> P.triple2)) |
305 >> (Toplevel.theory o Method.method_setup)); |
321 >> (Toplevel.theory o Method.method_setup)); |
306 |
322 |
307 val declarationP = |
323 val _ = |
308 OuterSyntax.command "declaration" "generic ML declaration" (K.tag_ml K.thy_decl) |
324 OuterSyntax.command "declaration" "generic ML declaration" (K.tag_ml K.thy_decl) |
309 (P.opt_target -- P.text |
325 (P.opt_target -- P.text |
310 >> (fn (loc, txt) => Toplevel.local_theory loc (IsarCmd.declaration txt))); |
326 >> (fn (loc, txt) => Toplevel.local_theory loc (IsarCmd.declaration txt))); |
311 |
327 |
312 val simproc_setupP = |
328 val _ = |
313 OuterSyntax.command "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl) |
329 OuterSyntax.command "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl) |
314 (P.opt_target -- |
330 (P.opt_target -- |
315 P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") -- P.text -- |
331 P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") -- P.text -- |
316 Scan.optional (P.$$$ "identifier" |-- Scan.repeat1 P.xname) [] |
332 Scan.optional (P.$$$ "identifier" |-- Scan.repeat1 P.xname) [] |
317 >> (fn ((((loc, a), b), c), d) => Toplevel.local_theory loc (IsarCmd.simproc_setup a b c d))); |
333 >> (fn ((((loc, a), b), c), d) => Toplevel.local_theory loc (IsarCmd.simproc_setup a b c d))); |
319 |
335 |
320 (* translation functions *) |
336 (* translation functions *) |
321 |
337 |
322 val trfun = P.opt_keyword "advanced" -- P.text; |
338 val trfun = P.opt_keyword "advanced" -- P.text; |
323 |
339 |
324 val parse_ast_translationP = |
340 val _ = |
325 OuterSyntax.command "parse_ast_translation" "install parse ast translation functions" |
341 OuterSyntax.command "parse_ast_translation" "install parse ast translation functions" |
326 (K.tag_ml K.thy_decl) |
342 (K.tag_ml K.thy_decl) |
327 (trfun >> (Toplevel.theory o IsarCmd.parse_ast_translation)); |
343 (trfun >> (Toplevel.theory o IsarCmd.parse_ast_translation)); |
328 |
344 |
329 val parse_translationP = |
345 val _ = |
330 OuterSyntax.command "parse_translation" "install parse translation functions" |
346 OuterSyntax.command "parse_translation" "install parse translation functions" |
331 (K.tag_ml K.thy_decl) |
347 (K.tag_ml K.thy_decl) |
332 (trfun >> (Toplevel.theory o IsarCmd.parse_translation)); |
348 (trfun >> (Toplevel.theory o IsarCmd.parse_translation)); |
333 |
349 |
334 val print_translationP = |
350 val _ = |
335 OuterSyntax.command "print_translation" "install print translation functions" |
351 OuterSyntax.command "print_translation" "install print translation functions" |
336 (K.tag_ml K.thy_decl) |
352 (K.tag_ml K.thy_decl) |
337 (trfun >> (Toplevel.theory o IsarCmd.print_translation)); |
353 (trfun >> (Toplevel.theory o IsarCmd.print_translation)); |
338 |
354 |
339 val typed_print_translationP = |
355 val _ = |
340 OuterSyntax.command "typed_print_translation" "install typed print translation functions" |
356 OuterSyntax.command "typed_print_translation" "install typed print translation functions" |
341 (K.tag_ml K.thy_decl) |
357 (K.tag_ml K.thy_decl) |
342 (trfun >> (Toplevel.theory o IsarCmd.typed_print_translation)); |
358 (trfun >> (Toplevel.theory o IsarCmd.typed_print_translation)); |
343 |
359 |
344 val print_ast_translationP = |
360 val _ = |
345 OuterSyntax.command "print_ast_translation" "install print ast translation functions" |
361 OuterSyntax.command "print_ast_translation" "install print ast translation functions" |
346 (K.tag_ml K.thy_decl) |
362 (K.tag_ml K.thy_decl) |
347 (trfun >> (Toplevel.theory o IsarCmd.print_ast_translation)); |
363 (trfun >> (Toplevel.theory o IsarCmd.print_ast_translation)); |
348 |
364 |
349 val token_translationP = |
365 val _ = |
350 OuterSyntax.command "token_translation" "install token translation functions" |
366 OuterSyntax.command "token_translation" "install token translation functions" |
351 (K.tag_ml K.thy_decl) |
367 (K.tag_ml K.thy_decl) |
352 (P.text >> (Toplevel.theory o IsarCmd.token_translation)); |
368 (P.text >> (Toplevel.theory o IsarCmd.token_translation)); |
353 |
369 |
354 |
370 |
355 (* oracles *) |
371 (* oracles *) |
356 |
372 |
357 val oracleP = |
373 val _ = |
358 OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl) |
374 OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl) |
359 (P.name -- (P.$$$ "(" |-- P.text --| P.$$$ ")" --| P.$$$ "=") |
375 (P.name -- (P.$$$ "(" |-- P.text --| P.$$$ ")" --| P.$$$ "=") |
360 -- P.text >> (fn ((x, y), z) => Toplevel.theory (IsarCmd.oracle x y z))); |
376 -- P.text >> (fn ((x, y), z) => Toplevel.theory (IsarCmd.oracle x y z))); |
361 |
377 |
362 |
378 |
363 (* local theories *) |
379 (* local theories *) |
364 |
380 |
365 val contextP = |
381 val _ = |
366 OuterSyntax.command "context" "enter local theory context" K.thy_decl |
382 OuterSyntax.command "context" "enter local theory context" K.thy_decl |
367 (P.name --| P.begin >> (fn name => |
383 (P.name --| P.begin >> (fn name => |
368 Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.init (SOME name)))); |
384 Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.init (SOME name)))); |
369 |
385 |
370 |
386 |
371 (* locales *) |
387 (* locales *) |
372 |
388 |
373 val locale_val = |
389 val locale_val = |
374 (SpecParse.locale_expr -- |
390 SpecParse.locale_expr -- |
375 Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] || |
391 Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] || |
376 Scan.repeat1 SpecParse.context_element >> pair Locale.empty); |
392 Scan.repeat1 SpecParse.context_element >> pair Locale.empty; |
377 |
393 |
378 val localeP = |
394 val _ = |
379 OuterSyntax.command "locale" "define named proof context" K.thy_decl |
395 OuterSyntax.command "locale" "define named proof context" K.thy_decl |
380 ((P.opt_keyword "open" >> (fn true => NONE | false => SOME "")) -- P.name |
396 ((P.opt_keyword "open" >> (fn true => NONE | false => SOME "")) -- |
381 -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, []) |
397 P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, []) -- P.opt_begin |
382 -- P.opt_begin |
|
383 >> (fn (((is_open, name), (expr, elems)), begin) => |
398 >> (fn (((is_open, name), (expr, elems)), begin) => |
384 (begin ? Toplevel.print) o Toplevel.begin_local_theory begin |
399 (begin ? Toplevel.print) o Toplevel.begin_local_theory begin |
385 (Locale.add_locale is_open name expr elems #-> TheoryTarget.begin))); |
400 (Locale.add_locale is_open name expr elems #-> TheoryTarget.begin))); |
386 |
401 |
387 val interpretationP = |
402 val _ = |
388 OuterSyntax.command "interpretation" |
403 OuterSyntax.command "interpretation" |
389 "prove and register interpretation of locale expression in theory or locale" K.thy_goal |
404 "prove and register interpretation of locale expression in theory or locale" K.thy_goal |
390 (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr |
405 (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr |
391 >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I)) || |
406 >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I)) || |
392 SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts |
407 SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts |
393 >> (fn ((x, y), z) => Toplevel.print o |
408 >> (fn ((x, y), z) => Toplevel.print o |
394 Toplevel.theory_to_proof (Locale.interpretation I (apfst (pair true) x) y z))); |
409 Toplevel.theory_to_proof (Locale.interpretation I (apfst (pair true) x) y z))); |
395 |
410 |
396 val interpretP = |
411 val _ = |
397 OuterSyntax.command "interpret" |
412 OuterSyntax.command "interpret" |
398 "prove and register interpretation of locale expression in proof context" |
413 "prove and register interpretation of locale expression in proof context" |
399 (K.tag_proof K.prf_goal) |
414 (K.tag_proof K.prf_goal) |
400 (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts |
415 (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts |
401 >> (fn ((x, y), z) => Toplevel.print o |
416 >> (fn ((x, y), z) => Toplevel.print o |
402 Toplevel.proof' (Locale.interpret Seq.single (apfst (pair true) x) y z))); |
417 Toplevel.proof' (Locale.interpret Seq.single (apfst (pair true) x) y z))); |
403 |
418 |
404 |
419 |
405 (* classes *) |
420 (* classes *) |
406 |
421 |
407 local |
422 val class_val = |
408 |
423 SpecParse.class_expr -- |
409 val class_subP = P.name -- Scan.repeat (P.$$$ "+" |-- P.name) >> (op ::); |
424 Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.locale_element)) [] || |
410 val class_bodyP = P.!!! (Scan.repeat1 SpecParse.locale_element); |
425 Scan.repeat1 SpecParse.locale_element >> pair []; |
411 |
426 |
412 in |
427 val _ = |
413 |
428 OuterSyntax.command "class" "define type class" K.thy_decl |
414 val classP = |
429 (P.name -- |
415 OuterSyntax.command "class" "define type class" K.thy_decl ( |
430 Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") [] -- (* FIXME ?? *) |
416 P.name |
431 Scan.optional (P.$$$ "(" |-- (P.$$$ "local_syntax" >> K true) --| P.$$$ ")") false -- (* FIXME ?? *) |
417 -- Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") [] |
432 (P.$$$ "=" |-- class_val) -- P.opt_begin |
418 -- Scan.optional (P.$$$ "(" |-- (P.$$$ "local_syntax" >> K true) --| P.$$$ ")") false |
|
419 --| P.$$$ "=" -- ( |
|
420 class_subP --| P.$$$ "+" -- class_bodyP |
|
421 || class_subP >> rpair [] |
|
422 || class_bodyP >> pair []) |
|
423 -- P.opt_begin |
|
424 >> (fn ((((bname, add_consts), local_syntax), (supclasses, elems)), begin) => |
433 >> (fn ((((bname, add_consts), local_syntax), (supclasses, elems)), begin) => |
425 Toplevel.begin_local_theory begin |
434 Toplevel.begin_local_theory begin |
426 (Class.class_cmd false bname supclasses elems add_consts #-> TheoryTarget.begin))); |
435 (Class.class_cmd false bname supclasses elems add_consts #-> TheoryTarget.begin))); |
427 |
436 |
428 val instanceP = |
437 val _ = |
429 OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal (( |
438 OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal |
430 P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) |
439 ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd || |
431 >> Class.classrel_cmd |
440 P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) |
432 || P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) |
441 >> Class.interpretation_in_class_cmd || (* FIXME ?? *) |
433 >> Class.interpretation_in_class_cmd |
442 P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop) |
434 || P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop) |
443 >> (fn (arities, defs) => Class.instance_cmd arities defs (fold Code.add_default_func (* FIXME ? *)))) |
435 >> (fn (arities, defs) => Class.instance_cmd arities defs (fold Code.add_default_func)) |
444 >> (Toplevel.print oo Toplevel.theory_to_proof)); |
436 ) >> (Toplevel.print oo Toplevel.theory_to_proof)); |
445 |
437 |
446 val _ = |
438 val instantiationP = |
447 OuterSyntax.command "instantiation" "prove type arity" K.thy_decl |
439 OuterSyntax.command "instantiation" "prove type arity" K.thy_decl ( |
448 (P.and_list1 P.arity -- P.opt_begin |
440 P.and_list1 P.arity -- P.opt_begin |
449 >> (fn (arities, begin) => (begin ? Toplevel.print) o |
441 >> (fn (arities, begin) => (begin ? Toplevel.print) |
450 Toplevel.begin_local_theory begin (Instance.begin_instantiation_cmd arities))); |
442 o Toplevel.begin_local_theory begin |
451 |
443 (Instance.begin_instantiation_cmd arities))); |
452 val _ = (* FIXME incorporate into "instance" *) |
444 |
|
445 val instance_proofP = |
|
446 OuterSyntax.command "instance_proof" "prove type arity relation" K.thy_goal |
453 OuterSyntax.command "instance_proof" "prove type arity relation" K.thy_goal |
447 (Scan.succeed ((Toplevel.print oo Toplevel.local_theory_to_proof NONE) Instance.proof_instantiation)); |
454 (Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE Instance.proof_instantiation)); |
448 |
|
449 end; |
|
450 |
455 |
451 |
456 |
452 (* code generation *) |
457 (* code generation *) |
453 |
458 |
454 val code_datatypeP = |
459 val _ = |
455 OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl |
460 OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl |
456 (Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd)); |
461 (Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd)); |
457 |
462 |
458 |
463 |
459 |
464 |
468 SpecParse.general_statement >> (fn ((loc, a), (elems, concl)) => |
473 SpecParse.general_statement >> (fn ((loc, a), (elems, concl)) => |
469 (Toplevel.print o |
474 (Toplevel.print o |
470 Toplevel.local_theory_to_proof' loc |
475 Toplevel.local_theory_to_proof' loc |
471 (Specification.theorem kind NONE (K I) a elems concl)))); |
476 (Specification.theorem kind NONE (K I) a elems concl)))); |
472 |
477 |
473 val theoremP = gen_theorem Thm.theoremK; |
478 val _ = gen_theorem Thm.theoremK; |
474 val lemmaP = gen_theorem Thm.lemmaK; |
479 val _ = gen_theorem Thm.lemmaK; |
475 val corollaryP = gen_theorem Thm.corollaryK; |
480 val _ = gen_theorem Thm.corollaryK; |
476 |
481 |
477 val haveP = |
482 val _ = |
478 OuterSyntax.command "have" "state local goal" |
483 OuterSyntax.command "have" "state local goal" |
479 (K.tag_proof K.prf_goal) |
484 (K.tag_proof K.prf_goal) |
480 (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have)); |
485 (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have)); |
481 |
486 |
482 val henceP = |
487 val _ = |
483 OuterSyntax.command "hence" "abbreviates \"then have\"" |
488 OuterSyntax.command "hence" "abbreviates \"then have\"" |
484 (K.tag_proof K.prf_goal) |
489 (K.tag_proof K.prf_goal) |
485 (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence)); |
490 (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence)); |
486 |
491 |
487 val showP = |
492 val _ = |
488 OuterSyntax.command "show" "state local goal, solving current obligation" |
493 OuterSyntax.command "show" "state local goal, solving current obligation" |
489 (K.tag_proof K.prf_asm_goal) |
494 (K.tag_proof K.prf_asm_goal) |
490 (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show)); |
495 (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show)); |
491 |
496 |
492 val thusP = |
497 val _ = |
493 OuterSyntax.command "thus" "abbreviates \"then show\"" |
498 OuterSyntax.command "thus" "abbreviates \"then show\"" |
494 (K.tag_proof K.prf_asm_goal) |
499 (K.tag_proof K.prf_asm_goal) |
495 (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus)); |
500 (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus)); |
496 |
501 |
497 |
502 |
498 (* facts *) |
503 (* facts *) |
499 |
504 |
500 val facts = P.and_list1 SpecParse.xthms1; |
505 val facts = P.and_list1 SpecParse.xthms1; |
501 |
506 |
502 val thenP = |
507 val _ = |
503 OuterSyntax.command "then" "forward chaining" |
508 OuterSyntax.command "then" "forward chaining" |
504 (K.tag_proof K.prf_chain) |
509 (K.tag_proof K.prf_chain) |
505 (Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain)); |
510 (Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain)); |
506 |
511 |
507 val fromP = |
512 val _ = |
508 OuterSyntax.command "from" "forward chaining from given facts" |
513 OuterSyntax.command "from" "forward chaining from given facts" |
509 (K.tag_proof K.prf_chain) |
514 (K.tag_proof K.prf_chain) |
510 (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss))); |
515 (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss))); |
511 |
516 |
512 val withP = |
517 val _ = |
513 OuterSyntax.command "with" "forward chaining from given and current facts" |
518 OuterSyntax.command "with" "forward chaining from given and current facts" |
514 (K.tag_proof K.prf_chain) |
519 (K.tag_proof K.prf_chain) |
515 (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss))); |
520 (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss))); |
516 |
521 |
517 val noteP = |
522 val _ = |
518 OuterSyntax.command "note" "define facts" |
523 OuterSyntax.command "note" "define facts" |
519 (K.tag_proof K.prf_decl) |
524 (K.tag_proof K.prf_decl) |
520 (SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss))); |
525 (SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss))); |
521 |
526 |
522 val usingP = |
527 val _ = |
523 OuterSyntax.command "using" "augment goal facts" |
528 OuterSyntax.command "using" "augment goal facts" |
524 (K.tag_proof K.prf_decl) |
529 (K.tag_proof K.prf_decl) |
525 (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using))); |
530 (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using))); |
526 |
531 |
527 val unfoldingP = |
532 val _ = |
528 OuterSyntax.command "unfolding" "unfold definitions in goal and facts" |
533 OuterSyntax.command "unfolding" "unfold definitions in goal and facts" |
529 (K.tag_proof K.prf_decl) |
534 (K.tag_proof K.prf_decl) |
530 (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding))); |
535 (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding))); |
531 |
536 |
532 |
537 |
533 (* proof context *) |
538 (* proof context *) |
534 |
539 |
535 val fixP = |
540 val _ = |
536 OuterSyntax.command "fix" "fix local variables (Skolem constants)" |
541 OuterSyntax.command "fix" "fix local variables (Skolem constants)" |
537 (K.tag_proof K.prf_asm) |
542 (K.tag_proof K.prf_asm) |
538 (P.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix))); |
543 (P.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix))); |
539 |
544 |
540 val assumeP = |
545 val _ = |
541 OuterSyntax.command "assume" "assume propositions" |
546 OuterSyntax.command "assume" "assume propositions" |
542 (K.tag_proof K.prf_asm) |
547 (K.tag_proof K.prf_asm) |
543 (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume))); |
548 (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume))); |
544 |
549 |
545 val presumeP = |
550 val _ = |
546 OuterSyntax.command "presume" "assume propositions, to be established later" |
551 OuterSyntax.command "presume" "assume propositions, to be established later" |
547 (K.tag_proof K.prf_asm) |
552 (K.tag_proof K.prf_asm) |
548 (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume))); |
553 (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume))); |
549 |
554 |
550 val defP = |
555 val _ = |
551 OuterSyntax.command "def" "local definition" |
556 OuterSyntax.command "def" "local definition" |
552 (K.tag_proof K.prf_asm) |
557 (K.tag_proof K.prf_asm) |
553 (P.and_list1 |
558 (P.and_list1 |
554 (SpecParse.opt_thm_name ":" -- |
559 (SpecParse.opt_thm_name ":" -- |
555 ((P.name -- P.opt_mixfix) -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp))) |
560 ((P.name -- P.opt_mixfix) -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp))) |
556 >> (Toplevel.print oo (Toplevel.proof o Proof.def))); |
561 >> (Toplevel.print oo (Toplevel.proof o Proof.def))); |
557 |
562 |
558 val obtainP = |
563 val _ = |
559 OuterSyntax.command "obtain" "generalized existence" |
564 OuterSyntax.command "obtain" "generalized existence" |
560 (K.tag_proof K.prf_asm_goal) |
565 (K.tag_proof K.prf_asm_goal) |
561 (P.parname -- Scan.optional (P.fixes --| P.where_) [] -- SpecParse.statement |
566 (P.parname -- Scan.optional (P.fixes --| P.where_) [] -- SpecParse.statement |
562 >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain x y z))); |
567 >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain x y z))); |
563 |
568 |
564 val guessP = |
569 val _ = |
565 OuterSyntax.command "guess" "wild guessing (unstructured)" |
570 OuterSyntax.command "guess" "wild guessing (unstructured)" |
566 (K.tag_proof K.prf_asm_goal) |
571 (K.tag_proof K.prf_asm_goal) |
567 (Scan.optional P.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess))); |
572 (Scan.optional P.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess))); |
568 |
573 |
569 val letP = |
574 val _ = |
570 OuterSyntax.command "let" "bind text variables" |
575 OuterSyntax.command "let" "bind text variables" |
571 (K.tag_proof K.prf_decl) |
576 (K.tag_proof K.prf_decl) |
572 (P.and_list1 (P.enum1 "and" P.term -- (P.$$$ "=" |-- P.term)) |
577 (P.and_list1 (P.enum1 "and" P.term -- (P.$$$ "=" |-- P.term)) |
573 >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind))); |
578 >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind))); |
574 |
579 |
575 val case_spec = |
580 val case_spec = |
576 (P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 (P.maybe P.name) --| P.$$$ ")") || |
581 (P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 (P.maybe P.name) --| P.$$$ ")") || |
577 P.xname >> rpair []) -- SpecParse.opt_attribs >> P.triple1; |
582 P.xname >> rpair []) -- SpecParse.opt_attribs >> P.triple1; |
578 |
583 |
579 val caseP = |
584 val _ = |
580 OuterSyntax.command "case" "invoke local context" |
585 OuterSyntax.command "case" "invoke local context" |
581 (K.tag_proof K.prf_asm) |
586 (K.tag_proof K.prf_asm) |
582 (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case))); |
587 (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case))); |
583 |
588 |
584 |
589 |
585 (* proof structure *) |
590 (* proof structure *) |
586 |
591 |
587 val begin_blockP = |
592 val _ = |
588 OuterSyntax.command "{" "begin explicit proof block" |
593 OuterSyntax.command "{" "begin explicit proof block" |
589 (K.tag_proof K.prf_open) |
594 (K.tag_proof K.prf_open) |
590 (Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block)); |
595 (Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block)); |
591 |
596 |
592 val end_blockP = |
597 val _ = |
593 OuterSyntax.command "}" "end explicit proof block" |
598 OuterSyntax.command "}" "end explicit proof block" |
594 (K.tag_proof K.prf_close) |
599 (K.tag_proof K.prf_close) |
595 (Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block)); |
600 (Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block)); |
596 |
601 |
597 val nextP = |
602 val _ = |
598 OuterSyntax.command "next" "enter next proof block" |
603 OuterSyntax.command "next" "enter next proof block" |
599 (K.tag_proof K.prf_block) |
604 (K.tag_proof K.prf_block) |
600 (Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block)); |
605 (Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block)); |
601 |
606 |
602 |
607 |
603 (* end proof *) |
608 (* end proof *) |
604 |
609 |
605 val qedP = |
610 val _ = |
606 OuterSyntax.command "qed" "conclude (sub-)proof" |
611 OuterSyntax.command "qed" "conclude (sub-)proof" |
607 (K.tag_proof K.qed_block) |
612 (K.tag_proof K.qed_block) |
608 (Scan.option Method.parse >> (Toplevel.print3 oo IsarCmd.qed)); |
613 (Scan.option Method.parse >> (Toplevel.print3 oo IsarCmd.qed)); |
609 |
614 |
610 val terminal_proofP = |
615 val _ = |
611 OuterSyntax.command "by" "terminal backward proof" |
616 OuterSyntax.command "by" "terminal backward proof" |
612 (K.tag_proof K.qed) |
617 (K.tag_proof K.qed) |
613 (Method.parse -- Scan.option Method.parse >> (Toplevel.print3 oo IsarCmd.terminal_proof)); |
618 (Method.parse -- Scan.option Method.parse >> (Toplevel.print3 oo IsarCmd.terminal_proof)); |
614 |
619 |
615 val default_proofP = |
620 val _ = |
616 OuterSyntax.command ".." "default proof" |
621 OuterSyntax.command ".." "default proof" |
617 (K.tag_proof K.qed) |
622 (K.tag_proof K.qed) |
618 (Scan.succeed (Toplevel.print3 o IsarCmd.default_proof)); |
623 (Scan.succeed (Toplevel.print3 o IsarCmd.default_proof)); |
619 |
624 |
620 val immediate_proofP = |
625 val _ = |
621 OuterSyntax.command "." "immediate proof" |
626 OuterSyntax.command "." "immediate proof" |
622 (K.tag_proof K.qed) |
627 (K.tag_proof K.qed) |
623 (Scan.succeed (Toplevel.print3 o IsarCmd.immediate_proof)); |
628 (Scan.succeed (Toplevel.print3 o IsarCmd.immediate_proof)); |
624 |
629 |
625 val done_proofP = |
630 val _ = |
626 OuterSyntax.command "done" "done proof" |
631 OuterSyntax.command "done" "done proof" |
627 (K.tag_proof K.qed) |
632 (K.tag_proof K.qed) |
628 (Scan.succeed (Toplevel.print3 o IsarCmd.done_proof)); |
633 (Scan.succeed (Toplevel.print3 o IsarCmd.done_proof)); |
629 |
634 |
630 val skip_proofP = |
635 val _ = |
631 OuterSyntax.improper_command "sorry" "skip proof (quick-and-dirty mode only!)" |
636 OuterSyntax.improper_command "sorry" "skip proof (quick-and-dirty mode only!)" |
632 (K.tag_proof K.qed) |
637 (K.tag_proof K.qed) |
633 (Scan.succeed (Toplevel.print3 o IsarCmd.skip_proof)); |
638 (Scan.succeed (Toplevel.print3 o IsarCmd.skip_proof)); |
634 |
639 |
635 val forget_proofP = |
640 val _ = |
636 OuterSyntax.command "oops" "forget proof" |
641 OuterSyntax.command "oops" "forget proof" |
637 (K.tag_proof K.qed_global) |
642 (K.tag_proof K.qed_global) |
638 (Scan.succeed Toplevel.forget_proof); |
643 (Scan.succeed Toplevel.forget_proof); |
639 |
644 |
640 |
645 |
641 (* proof steps *) |
646 (* proof steps *) |
642 |
647 |
643 val deferP = |
648 val _ = |
644 OuterSyntax.command "defer" "shuffle internal proof state" |
649 OuterSyntax.command "defer" "shuffle internal proof state" |
645 (K.tag_proof K.prf_script) |
650 (K.tag_proof K.prf_script) |
646 (Scan.option P.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer))); |
651 (Scan.option P.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer))); |
647 |
652 |
648 val preferP = |
653 val _ = |
649 OuterSyntax.command "prefer" "shuffle internal proof state" |
654 OuterSyntax.command "prefer" "shuffle internal proof state" |
650 (K.tag_proof K.prf_script) |
655 (K.tag_proof K.prf_script) |
651 (P.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.prefer))); |
656 (P.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.prefer))); |
652 |
657 |
653 val applyP = |
658 val _ = |
654 OuterSyntax.command "apply" "initial refinement step (unstructured)" |
659 OuterSyntax.command "apply" "initial refinement step (unstructured)" |
655 (K.tag_proof K.prf_script) |
660 (K.tag_proof K.prf_script) |
656 (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply))); |
661 (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply))); |
657 |
662 |
658 val apply_endP = |
663 val _ = |
659 OuterSyntax.command "apply_end" "terminal refinement (unstructured)" |
664 OuterSyntax.command "apply_end" "terminal refinement (unstructured)" |
660 (K.tag_proof K.prf_script) |
665 (K.tag_proof K.prf_script) |
661 (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end))); |
666 (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end))); |
662 |
667 |
663 val proofP = |
668 val _ = |
664 OuterSyntax.command "proof" "backward proof" |
669 OuterSyntax.command "proof" "backward proof" |
665 (K.tag_proof K.prf_block) |
670 (K.tag_proof K.prf_block) |
666 (Scan.option Method.parse >> (fn m => Toplevel.print o |
671 (Scan.option Method.parse >> (fn m => Toplevel.print o |
667 Toplevel.actual_proof (ProofHistory.applys (Proof.proof m)) o |
672 Toplevel.actual_proof (ProofHistory.applys (Proof.proof m)) o |
668 Toplevel.skip_proof (History.apply (fn i => i + 1)))); |
673 Toplevel.skip_proof (History.apply (fn i => i + 1)))); |
671 (* calculational proof commands *) |
676 (* calculational proof commands *) |
672 |
677 |
673 val calc_args = |
678 val calc_args = |
674 Scan.option (P.$$$ "(" |-- P.!!! ((SpecParse.xthms1 --| P.$$$ ")"))); |
679 Scan.option (P.$$$ "(" |-- P.!!! ((SpecParse.xthms1 --| P.$$$ ")"))); |
675 |
680 |
676 val alsoP = |
681 val _ = |
677 OuterSyntax.command "also" "combine calculation and current facts" |
682 OuterSyntax.command "also" "combine calculation and current facts" |
678 (K.tag_proof K.prf_decl) |
683 (K.tag_proof K.prf_decl) |
679 (calc_args >> (Toplevel.proofs' o Calculation.also)); |
684 (calc_args >> (Toplevel.proofs' o Calculation.also)); |
680 |
685 |
681 val finallyP = |
686 val _ = |
682 OuterSyntax.command "finally" "combine calculation and current facts, exhibit result" |
687 OuterSyntax.command "finally" "combine calculation and current facts, exhibit result" |
683 (K.tag_proof K.prf_chain) |
688 (K.tag_proof K.prf_chain) |
684 (calc_args >> (Toplevel.proofs' o Calculation.finally_)); |
689 (calc_args >> (Toplevel.proofs' o Calculation.finally_)); |
685 |
690 |
686 val moreoverP = |
691 val _ = |
687 OuterSyntax.command "moreover" "augment calculation by current facts" |
692 OuterSyntax.command "moreover" "augment calculation by current facts" |
688 (K.tag_proof K.prf_decl) |
693 (K.tag_proof K.prf_decl) |
689 (Scan.succeed (Toplevel.proof' Calculation.moreover)); |
694 (Scan.succeed (Toplevel.proof' Calculation.moreover)); |
690 |
695 |
691 val ultimatelyP = |
696 val _ = |
692 OuterSyntax.command "ultimately" "augment calculation by current facts, exhibit result" |
697 OuterSyntax.command "ultimately" "augment calculation by current facts, exhibit result" |
693 (K.tag_proof K.prf_chain) |
698 (K.tag_proof K.prf_chain) |
694 (Scan.succeed (Toplevel.proof' Calculation.ultimately)); |
699 (Scan.succeed (Toplevel.proof' Calculation.ultimately)); |
695 |
700 |
696 |
701 |
697 (* proof navigation *) |
702 (* proof navigation *) |
698 |
703 |
699 val backP = |
704 val _ = |
700 OuterSyntax.command "back" "backtracking of proof command" |
705 OuterSyntax.command "back" "backtracking of proof command" |
701 (K.tag_proof K.prf_script) |
706 (K.tag_proof K.prf_script) |
702 (Scan.succeed (Toplevel.print o IsarCmd.back)); |
707 (Scan.succeed (Toplevel.print o IsarCmd.back)); |
703 |
708 |
704 |
709 |
705 (* history *) |
710 (* history *) |
706 |
711 |
707 val cannot_undoP = |
712 val _ = |
708 OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control |
713 OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control |
709 (P.name >> (Toplevel.no_timing oo IsarCmd.cannot_undo)); |
714 (P.name >> (Toplevel.no_timing oo IsarCmd.cannot_undo)); |
710 |
715 |
711 val redoP = |
716 val _ = |
712 OuterSyntax.improper_command "redo" "redo last command" K.control |
717 OuterSyntax.improper_command "redo" "redo last command" K.control |
713 (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.redo)); |
718 (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.redo)); |
714 |
719 |
715 val undos_proofP = |
720 val _ = |
716 OuterSyntax.improper_command "undos_proof" "undo last proof commands" K.control |
721 OuterSyntax.improper_command "undos_proof" "undo last proof commands" K.control |
717 (P.nat >> ((Toplevel.no_timing o Toplevel.print) oo IsarCmd.undos_proof)); |
722 (P.nat >> ((Toplevel.no_timing o Toplevel.print) oo IsarCmd.undos_proof)); |
718 |
723 |
719 val undoP = |
724 val _ = |
720 OuterSyntax.improper_command "undo" "undo last command" K.control |
725 OuterSyntax.improper_command "undo" "undo last command" K.control |
721 (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.undo)); |
726 (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.undo)); |
722 |
727 |
723 val killP = |
728 val _ = |
724 OuterSyntax.improper_command "kill" "kill current history node" K.control |
729 OuterSyntax.improper_command "kill" "kill current history node" K.control |
725 (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.kill)); |
730 (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.kill)); |
726 |
731 |
727 |
732 |
728 |
733 |
729 (** diagnostic commands (for interactive mode only) **) |
734 (** diagnostic commands (for interactive mode only) **) |
730 |
735 |
731 val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) []; |
736 val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) []; |
732 val opt_bang = Scan.optional (P.$$$ "!" >> K true) false; |
737 val opt_bang = Scan.optional (P.$$$ "!" >> K true) false; |
733 |
738 |
734 val pretty_setmarginP = |
739 val _ = |
735 OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing" |
740 OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing" |
736 K.diag (P.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin)); |
741 K.diag (P.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin)); |
737 |
742 |
738 val helpP = |
743 val _ = |
739 OuterSyntax.improper_command "help" "print outer syntax commands" K.diag |
744 OuterSyntax.improper_command "help" "print outer syntax commands" K.diag |
740 (Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands)); |
745 (Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands)); |
741 |
746 |
742 val print_commandsP = |
747 val _ = |
743 OuterSyntax.improper_command "print_commands" "print outer syntax commands" K.diag |
748 OuterSyntax.improper_command "print_commands" "print outer syntax commands" K.diag |
744 (Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands)); |
749 (Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands)); |
745 |
750 |
746 val print_configsP = |
751 val _ = |
747 OuterSyntax.improper_command "print_configs" "print configuration options" K.diag |
752 OuterSyntax.improper_command "print_configs" "print configuration options" K.diag |
748 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_configs)); |
753 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_configs)); |
749 |
754 |
750 val print_contextP = |
755 val _ = |
751 OuterSyntax.improper_command "print_context" "print theory context name" K.diag |
756 OuterSyntax.improper_command "print_context" "print theory context name" K.diag |
752 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_context)); |
757 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_context)); |
753 |
758 |
754 val print_theoryP = |
759 val _ = |
755 OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag |
760 OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag |
756 (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory)); |
761 (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory)); |
757 |
762 |
758 val print_syntaxP = |
763 val _ = |
759 OuterSyntax.improper_command "print_syntax" "print inner syntax of context (verbose!)" K.diag |
764 OuterSyntax.improper_command "print_syntax" "print inner syntax of context (verbose!)" K.diag |
760 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax)); |
765 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax)); |
761 |
766 |
762 val print_abbrevsP = |
767 val _ = |
763 OuterSyntax.improper_command "print_abbrevs" "print constant abbreviation of context" K.diag |
768 OuterSyntax.improper_command "print_abbrevs" "print constant abbreviation of context" K.diag |
764 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_abbrevs)); |
769 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_abbrevs)); |
765 |
770 |
766 val print_theoremsP = |
771 val _ = |
767 OuterSyntax.improper_command "print_theorems" |
772 OuterSyntax.improper_command "print_theorems" |
768 "print theorems of local theory or proof context" K.diag |
773 "print theorems of local theory or proof context" K.diag |
769 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_theorems)); |
774 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_theorems)); |
770 |
775 |
771 val print_localesP = |
776 val _ = |
772 OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag |
777 OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag |
773 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_locales)); |
778 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_locales)); |
774 |
779 |
775 val print_classesP = |
780 val _ = |
776 OuterSyntax.improper_command "print_classes" "print classes of this theory" K.diag |
781 OuterSyntax.improper_command "print_classes" "print classes of this theory" K.diag |
777 (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory |
782 (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory |
778 o Toplevel.keep (Class.print_classes o Toplevel.theory_of))); |
783 o Toplevel.keep (Class.print_classes o Toplevel.theory_of))); |
779 |
784 |
780 val print_localeP = |
785 val _ = |
781 OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag |
786 OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag |
782 (opt_bang -- locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale)); |
787 (opt_bang -- locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale)); |
783 |
788 |
784 val print_registrationsP = |
789 val _ = |
785 OuterSyntax.improper_command "print_interps" |
790 OuterSyntax.improper_command "print_interps" |
786 "print interpretations of named locale" K.diag |
791 "print interpretations of named locale" K.diag |
787 (Scan.optional (P.$$$ "!" >> K true) false -- P.xname |
792 (Scan.optional (P.$$$ "!" >> K true) false -- P.xname |
788 >> (Toplevel.no_timing oo uncurry IsarCmd.print_registrations)); |
793 >> (Toplevel.no_timing oo uncurry IsarCmd.print_registrations)); |
789 |
794 |
790 val print_attributesP = |
795 val _ = |
791 OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag |
796 OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag |
792 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes)); |
797 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes)); |
793 |
798 |
794 val print_simpsetP = |
799 val _ = |
795 OuterSyntax.improper_command "print_simpset" "print context of Simplifier" K.diag |
800 OuterSyntax.improper_command "print_simpset" "print context of Simplifier" K.diag |
796 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_simpset)); |
801 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_simpset)); |
797 |
802 |
798 val print_rulesP = |
803 val _ = |
799 OuterSyntax.improper_command "print_rules" "print intro/elim rules" K.diag |
804 OuterSyntax.improper_command "print_rules" "print intro/elim rules" K.diag |
800 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_rules)); |
805 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_rules)); |
801 |
806 |
802 val print_trans_rulesP = |
807 val _ = |
803 OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" K.diag |
808 OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" K.diag |
804 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules)); |
809 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules)); |
805 |
810 |
806 val print_methodsP = |
811 val _ = |
807 OuterSyntax.improper_command "print_methods" "print methods of this theory" K.diag |
812 OuterSyntax.improper_command "print_methods" "print methods of this theory" K.diag |
808 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods)); |
813 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods)); |
809 |
814 |
810 val print_antiquotationsP = |
815 val _ = |
811 OuterSyntax.improper_command "print_antiquotations" "print antiquotations (global)" K.diag |
816 OuterSyntax.improper_command "print_antiquotations" "print antiquotations (global)" K.diag |
812 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations)); |
817 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations)); |
813 |
818 |
814 val thy_depsP = |
819 val _ = |
815 OuterSyntax.improper_command "thy_deps" "visualize theory dependencies" |
820 OuterSyntax.improper_command "thy_deps" "visualize theory dependencies" |
816 K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.thy_deps)); |
821 K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.thy_deps)); |
817 |
822 |
818 val class_depsP = |
823 val _ = |
819 OuterSyntax.improper_command "class_deps" "visualize class dependencies" |
824 OuterSyntax.improper_command "class_deps" "visualize class dependencies" |
820 K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps)); |
825 K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps)); |
821 |
826 |
822 val thm_depsP = |
827 val _ = |
823 OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies" |
828 OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies" |
824 K.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps)); |
829 K.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps)); |
825 |
830 |
826 local |
831 local |
827 |
832 |
838 (P.$$$ "(" |-- |
843 (P.$$$ "(" |-- |
839 P.!!! (Scan.option P.nat -- Scan.optional (P.reserved "with_dups" >> K false) true |
844 P.!!! (Scan.option P.nat -- Scan.optional (P.reserved "with_dups" >> K false) true |
840 --| P.$$$ ")")) (NONE, true); |
845 --| P.$$$ ")")) (NONE, true); |
841 in |
846 in |
842 |
847 |
843 val find_theoremsP = |
848 val _ = |
844 OuterSyntax.improper_command "find_theorems" "print theorems meeting specified criteria" K.diag |
849 OuterSyntax.improper_command "find_theorems" "print theorems meeting specified criteria" K.diag |
845 (options -- Scan.repeat (((Scan.option P.minus >> is_none) -- criterion)) |
850 (options -- Scan.repeat (((Scan.option P.minus >> is_none) -- criterion)) |
846 >> (Toplevel.no_timing oo IsarCmd.find_theorems)); |
851 >> (Toplevel.no_timing oo IsarCmd.find_theorems)); |
847 |
852 |
848 end; |
853 end; |
849 |
854 |
850 val print_bindsP = |
855 val _ = |
851 OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag |
856 OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag |
852 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds)); |
857 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds)); |
853 |
858 |
854 val print_factsP = |
859 val _ = |
855 OuterSyntax.improper_command "print_facts" "print facts of proof context" K.diag |
860 OuterSyntax.improper_command "print_facts" "print facts of proof context" K.diag |
856 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_facts)); |
861 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_facts)); |
857 |
862 |
858 val print_casesP = |
863 val _ = |
859 OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag |
864 OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag |
860 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases)); |
865 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases)); |
861 |
866 |
862 val print_stmtsP = |
867 val _ = |
863 OuterSyntax.improper_command "print_statement" "print theorems as long statements" K.diag |
868 OuterSyntax.improper_command "print_statement" "print theorems as long statements" K.diag |
864 (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts)); |
869 (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts)); |
865 |
870 |
866 val print_thmsP = |
871 val _ = |
867 OuterSyntax.improper_command "thm" "print theorems" K.diag |
872 OuterSyntax.improper_command "thm" "print theorems" K.diag |
868 (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms)); |
873 (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms)); |
869 |
874 |
870 val print_prfsP = |
875 val _ = |
871 OuterSyntax.improper_command "prf" "print proof terms of theorems" K.diag |
876 OuterSyntax.improper_command "prf" "print proof terms of theorems" K.diag |
872 (opt_modes -- Scan.option SpecParse.xthms1 |
877 (opt_modes -- Scan.option SpecParse.xthms1 |
873 >> (Toplevel.no_timing oo IsarCmd.print_prfs false)); |
878 >> (Toplevel.no_timing oo IsarCmd.print_prfs false)); |
874 |
879 |
875 val print_full_prfsP = |
880 val _ = |
876 OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" K.diag |
881 OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" K.diag |
877 (opt_modes -- Scan.option SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true)); |
882 (opt_modes -- Scan.option SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true)); |
878 |
883 |
879 val print_propP = |
884 val _ = |
880 OuterSyntax.improper_command "prop" "read and print proposition" K.diag |
885 OuterSyntax.improper_command "prop" "read and print proposition" K.diag |
881 (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_prop)); |
886 (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_prop)); |
882 |
887 |
883 val print_termP = |
888 val _ = |
884 OuterSyntax.improper_command "term" "read and print term" K.diag |
889 OuterSyntax.improper_command "term" "read and print term" K.diag |
885 (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_term)); |
890 (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_term)); |
886 |
891 |
887 val print_typeP = |
892 val _ = |
888 OuterSyntax.improper_command "typ" "read and print type" K.diag |
893 OuterSyntax.improper_command "typ" "read and print type" K.diag |
889 (opt_modes -- P.typ >> (Toplevel.no_timing oo IsarCmd.print_type)); |
894 (opt_modes -- P.typ >> (Toplevel.no_timing oo IsarCmd.print_type)); |
890 |
895 |
891 val print_codesetupP = |
896 val _ = |
892 OuterSyntax.improper_command "print_codesetup" "print code generator setup of this theory" K.diag |
897 OuterSyntax.improper_command "print_codesetup" "print code generator setup of this theory" K.diag |
893 (Scan.succeed |
898 (Scan.succeed |
894 (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep |
899 (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep |
895 (Code.print_codesetup o Toplevel.theory_of))); |
900 (Code.print_codesetup o Toplevel.theory_of))); |
896 |
901 |
897 |
902 |
898 (** system commands (for interactive mode only) **) |
903 (** system commands (for interactive mode only) **) |
899 |
904 |
900 val cdP = |
905 val _ = |
901 OuterSyntax.improper_command "cd" "change current working directory" K.diag |
906 OuterSyntax.improper_command "cd" "change current working directory" K.diag |
902 (P.path >> (Toplevel.no_timing oo IsarCmd.cd)); |
907 (P.path >> (Toplevel.no_timing oo IsarCmd.cd)); |
903 |
908 |
904 val pwdP = |
909 val _ = |
905 OuterSyntax.improper_command "pwd" "print current working directory" K.diag |
910 OuterSyntax.improper_command "pwd" "print current working directory" K.diag |
906 (Scan.succeed (Toplevel.no_timing o IsarCmd.pwd)); |
911 (Scan.succeed (Toplevel.no_timing o IsarCmd.pwd)); |
907 |
912 |
908 val use_thyP = |
913 val _ = |
909 OuterSyntax.improper_command "use_thy" "use theory file" K.diag |
914 OuterSyntax.improper_command "use_thy" "use theory file" K.diag |
910 (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy)); |
915 (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy)); |
911 |
916 |
912 val touch_thyP = |
917 val _ = |
913 OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag |
918 OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag |
914 (P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy)); |
919 (P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy)); |
915 |
920 |
916 val touch_child_thysP = |
921 val _ = |
917 OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag |
922 OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag |
918 (P.name >> (Toplevel.no_timing oo IsarCmd.touch_child_thys)); |
923 (P.name >> (Toplevel.no_timing oo IsarCmd.touch_child_thys)); |
919 |
924 |
920 val remove_thyP = |
925 val _ = |
921 OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag |
926 OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag |
922 (P.name >> (Toplevel.no_timing oo IsarCmd.remove_thy)); |
927 (P.name >> (Toplevel.no_timing oo IsarCmd.remove_thy)); |
923 |
928 |
924 val kill_thyP = |
929 val _ = |
925 OuterSyntax.improper_command "kill_thy" "kill theory -- try to remove from loader database" |
930 OuterSyntax.improper_command "kill_thy" "kill theory -- try to remove from loader database" |
926 K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.kill_thy)); |
931 K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.kill_thy)); |
927 |
932 |
928 val display_draftsP = |
933 val _ = |
929 OuterSyntax.improper_command "display_drafts" "display raw source files with symbols" |
934 OuterSyntax.improper_command "display_drafts" "display raw source files with symbols" |
930 K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.display_drafts)); |
935 K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.display_drafts)); |
931 |
936 |
932 val print_draftsP = |
937 val _ = |
933 OuterSyntax.improper_command "print_drafts" "print raw source files with symbols" |
938 OuterSyntax.improper_command "print_drafts" "print raw source files with symbols" |
934 K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.print_drafts)); |
939 K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.print_drafts)); |
935 |
940 |
936 val opt_limits = |
941 val opt_limits = |
937 Scan.option P.nat -- Scan.option (P.$$$ "," |-- P.!!! P.nat); |
942 Scan.option P.nat -- Scan.option (P.$$$ "," |-- P.!!! P.nat); |
938 |
943 |
939 val prP = |
944 val _ = |
940 OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag |
945 OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag |
941 (opt_modes -- opt_limits >> (Toplevel.no_timing oo IsarCmd.pr)); |
946 (opt_modes -- opt_limits >> (Toplevel.no_timing oo IsarCmd.pr)); |
942 |
947 |
943 val disable_prP = |
948 val _ = |
944 OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" K.diag |
949 OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" K.diag |
945 (Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr)); |
950 (Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr)); |
946 |
951 |
947 val enable_prP = |
952 val _ = |
948 OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag |
953 OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag |
949 (Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr)); |
954 (Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr)); |
950 |
955 |
951 val commitP = |
956 val _ = |
952 OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag |
957 OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag |
953 (P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.use_commit)); |
958 (P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.use_commit)); |
954 |
959 |
955 val quitP = |
960 val _ = |
956 OuterSyntax.improper_command "quit" "quit Isabelle" K.control |
961 OuterSyntax.improper_command "quit" "quit Isabelle" K.control |
957 (P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit)); |
962 (P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit)); |
958 |
963 |
959 val exitP = |
964 val _ = |
960 OuterSyntax.improper_command "exit" "exit Isar loop" K.control |
965 OuterSyntax.improper_command "exit" "exit Isar loop" K.control |
961 (Scan.succeed (Toplevel.no_timing o IsarCmd.exit)); |
966 (Scan.succeed (Toplevel.no_timing o IsarCmd.exit)); |
962 |
967 |
963 val init_toplevelP = |
968 val _ = |
964 OuterSyntax.improper_command "init_toplevel" "restart Isar toplevel loop" K.control |
969 OuterSyntax.improper_command "init_toplevel" "restart Isar toplevel loop" K.control |
965 (Scan.succeed (Toplevel.no_timing o IsarCmd.init_toplevel)); |
970 (Scan.succeed (Toplevel.no_timing o IsarCmd.init_toplevel)); |
966 |
971 |
967 val welcomeP = |
972 val _ = |
968 OuterSyntax.improper_command "welcome" "print welcome message" K.diag |
973 OuterSyntax.improper_command "welcome" "print welcome message" K.diag |
969 (Scan.succeed (Toplevel.no_timing o IsarCmd.welcome)); |
974 (Scan.succeed (Toplevel.no_timing o IsarCmd.welcome)); |
970 |
975 |
971 |
|
972 |
|
973 (** the Pure outer syntax **) |
|
974 |
|
975 (*keep keywords consistent with the parsers, otherwise be prepared for |
|
976 unexpected errors*) |
|
977 |
|
978 val _ = OuterSyntax.add_keywords |
|
979 ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=", |
|
980 "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>", |
|
981 "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]", |
|
982 "advanced", "and", "assumes", "attach", "begin", "binder", "concl", |
|
983 "constrains", "defines", "fixes", "for", "identifier", "if", |
|
984 "imports", "in", "includes", "infix", "infixl", "infixr", "is", |
|
985 "local_syntax", "notes", "obtains", "open", "output", "overloaded", "shows", |
|
986 "structure", "unchecked", "uses", "where", "|"]; |
|
987 |
|
988 val _ = OuterSyntax.add_parsers [ |
|
989 (*theory structure*) |
|
990 theoryP, endP, |
|
991 (*markup commands*) |
|
992 headerP, chapterP, sectionP, subsectionP, subsubsectionP, textP, |
|
993 text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP, |
|
994 (*theory sections*) |
|
995 classesP, classrelP, defaultsortP, axclassP, typedeclP, typeabbrP, |
|
996 nontermP, aritiesP, judgmentP, constsP, finalconstsP, syntaxP, |
|
997 no_syntaxP, translationsP, no_translationsP, axiomsP, defsP, |
|
998 constdefsP, definitionP, abbreviationP, notationP, axiomatizationP, |
|
999 theoremsP, lemmasP, declareP, globalP, localP, hideP, useP, mlP, |
|
1000 ml_commandP, ml_setupP, setupP, method_setupP, declarationP, |
|
1001 simproc_setupP, parse_ast_translationP, parse_translationP, |
|
1002 print_translationP, typed_print_translationP, |
|
1003 print_ast_translationP, token_translationP, oracleP, contextP, |
|
1004 localeP, classP, instanceP, instantiationP, instance_proofP, |
|
1005 code_datatypeP, |
|
1006 (*proof commands*) |
|
1007 theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP, |
|
1008 assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP, |
|
1009 withP, noteP, usingP, unfoldingP, begin_blockP, end_blockP, nextP, |
|
1010 qedP, terminal_proofP, default_proofP, immediate_proofP, |
|
1011 done_proofP, skip_proofP, forget_proofP, deferP, preferP, applyP, |
|
1012 apply_endP, proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP, |
|
1013 cannot_undoP, redoP, undos_proofP, undoP, killP, interpretationP, |
|
1014 interpretP, |
|
1015 (*diagnostic commands*) |
|
1016 pretty_setmarginP, helpP, print_classesP, print_commandsP, |
|
1017 print_configsP, print_contextP, print_theoryP, print_syntaxP, |
|
1018 print_abbrevsP, print_factsP, print_theoremsP, print_localesP, |
|
1019 print_localeP, print_registrationsP, print_attributesP, |
|
1020 print_simpsetP, print_rulesP, print_trans_rulesP, print_methodsP, |
|
1021 print_antiquotationsP, thy_depsP, class_depsP, thm_depsP, |
|
1022 find_theoremsP, print_bindsP, print_casesP, print_stmtsP, |
|
1023 print_thmsP, print_prfsP, print_full_prfsP, print_propP, |
|
1024 print_termP, print_typeP, print_codesetupP, |
|
1025 (*system commands*) |
|
1026 cdP, pwdP, use_thyP, touch_thyP, touch_child_thysP, remove_thyP, |
|
1027 kill_thyP, display_draftsP, print_draftsP, prP, disable_prP, |
|
1028 enable_prP, commitP, quitP, exitP, init_toplevelP, welcomeP]; |
|
1029 |
|
1030 end; |
976 end; |