author  wenzelm 
Fri, 19 Jan 2007 22:08:26 +0100  
changeset 22117  505e040bdcdb 
parent 22088  4c53bb6e10e4 
child 22202  0544af1a5117 
permissions  rwrr 
5832  1 
(* Title: Pure/Isar/isar_syn.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

6353  5 
Isar/Pure outer syntax. 
5832  6 
*) 
7 

17353  8 
structure IsarSyn: sig end = 
5832  9 
struct 
10 

17068  11 
structure P = OuterParse and K = OuterKeyword; 
5832  12 

13 

14 
(** init and exit **) 

15 

16 
val theoryP = 

17068  17 
OuterSyntax.command "theory" "begin theory" (K.tag_theory K.thy_begin) 
21350  18 
(ThyHeader.args >> (Toplevel.print oo IsarCmd.theory)); 
5832  19 

20958  20 
val endP = 
21 
OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end) 

21004  22 
(Scan.succeed (Toplevel.exit o Toplevel.end_local_theory)); 
6687  23 

5832  24 

7749  25 
(** markup commands **) 
5832  26 

22117  27 
val headerP = OuterSyntax.markup_command ThyOutput.Markup "header" "theory header" K.diag 
12940  28 
(P.position P.text >> IsarCmd.add_header); 
6353  29 

22117  30 
val chapterP = OuterSyntax.markup_command ThyOutput.Markup "chapter" "chapter heading" 
31 
K.thy_heading (P.opt_target  P.position P.text >> IsarCmd.add_chapter); 

5958  32 

22117  33 
val sectionP = OuterSyntax.markup_command ThyOutput.Markup "section" "section heading" 
34 
K.thy_heading (P.opt_target  P.position P.text >> IsarCmd.add_section); 

5958  35 

22117  36 
val subsectionP = OuterSyntax.markup_command ThyOutput.Markup "subsection" "subsection heading" 
37 
K.thy_heading (P.opt_target  P.position P.text >> IsarCmd.add_subsection); 

5958  38 

7749  39 
val subsubsectionP = 
22117  40 
OuterSyntax.markup_command ThyOutput.Markup "subsubsection" "subsubsection heading" 
41 
K.thy_heading (P.opt_target  P.position P.text >> IsarCmd.add_subsubsection); 

5832  42 

22117  43 
val textP = OuterSyntax.markup_command ThyOutput.MarkupEnv "text" "formal comment (theory)" 
44 
K.thy_decl (P.opt_target  P.position P.text >> IsarCmd.add_text); 

7172  45 

22117  46 
val text_rawP = OuterSyntax.markup_command ThyOutput.Verbatim "text_raw" 
17264
c5b280a52a67
chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

47 
"raw document preparation text" 
c5b280a52a67
chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

48 
K.thy_decl (P.position P.text >> IsarCmd.add_text_raw); 
7172  49 

22117  50 
val sectP = OuterSyntax.markup_command ThyOutput.Markup "sect" "formal comment (proof)" 
17068  51 
(K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.add_sect); 
7172  52 

22117  53 
val subsectP = OuterSyntax.markup_command ThyOutput.Markup "subsect" "formal comment (proof)" 
17068  54 
(K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.add_subsect); 
7172  55 

22117  56 
val subsubsectP = OuterSyntax.markup_command ThyOutput.Markup "subsubsect" 
17068  57 
"formal comment (proof)" (K.tag_proof K.prf_heading) 
12940  58 
(P.position P.text >> IsarCmd.add_subsubsect); 
7172  59 

22117  60 
val txtP = OuterSyntax.markup_command ThyOutput.MarkupEnv "txt" "formal comment (proof)" 
17068  61 
(K.tag_proof K.prf_decl) (P.position P.text >> IsarCmd.add_txt); 
7172  62 

22117  63 
val txt_rawP = OuterSyntax.markup_command ThyOutput.Verbatim "txt_raw" 
17068  64 
"raw document preparation text (proof)" (K.tag_proof K.prf_decl) 
12940  65 
(P.position P.text >> IsarCmd.add_txt_raw); 
7775  66 

5832  67 

6886  68 

69 
(** theory sections **) 

70 

5832  71 
(* classes and sorts *) 
72 

73 
val classesP = 

6723  74 
OuterSyntax.command "classes" "declare type classes" K.thy_decl 
11101
014e7b5c77ba
support \<subseteq> syntax in classes/classrel/axclass/instance;
wenzelm
parents:
11017
diff
changeset

75 
(Scan.repeat1 (P.name  Scan.optional ((P.$$$ "\\<subseteq>"  P.$$$ "<")  
19516  76 
P.!!! (P.list1 P.xname)) []) >> (Toplevel.theory o fold AxClass.axiomatize_class)); 
5832  77 

78 
val classrelP = 

6723  79 
OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl 
14779  80 
(P.and_list1 (P.xname  ((P.$$$ "\\<subseteq>"  P.$$$ "<")  P.!!! P.xname)) 
19516  81 
>> (Toplevel.theory o AxClass.axiomatize_classrel)); 
5832  82 

83 
val defaultsortP = 

6723  84 
OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

85 
(P.sort >> (Toplevel.theory o Theory.add_defsort)); 
5832  86 

19245  87 
val axclassP = 
88 
OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl 

21462
74ddf3a522f8
added Isar syntax for adding parameters to axclasses
haftmann
parents:
21437
diff
changeset

89 
(P.name  Scan.optional ((P.$$$ "\\<subseteq>"  P.$$$ "<")  
74ddf3a522f8
added Isar syntax for adding parameters to axclasses
haftmann
parents:
21437
diff
changeset

90 
P.!!! (P.list1 P.xname)) [] 
21951  91 
 Scan.optional (P.$$$ "("  P.$$$ "attach"  Scan.repeat P.term  P.$$$ ")") [] 
22117  92 
 Scan.repeat (SpecParse.thm_name ":"  (P.prop >> single)) 
21462
74ddf3a522f8
added Isar syntax for adding parameters to axclasses
haftmann
parents:
21437
diff
changeset

93 
>> (fn ((x, y), z) => Toplevel.theory (snd o AxClass.define_class x y z))); 
19245  94 

5832  95 

96 
(* types *) 

97 

98 
val typedeclP = 

12624  99 
OuterSyntax.command "typedecl" "type declaration" K.thy_decl 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

100 
(P.type_args  P.name  P.opt_infix >> (fn ((args, a), mx) => 
16447  101 
Toplevel.theory (Theory.add_typedecls [(a, args, mx)]))); 
5832  102 

103 
val typeabbrP = 

6723  104 
OuterSyntax.command "types" "declare type abbreviations" K.thy_decl 
6727  105 
(Scan.repeat1 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

106 
(P.type_args  P.name  (P.$$$ "="  P.!!! (P.typ  P.opt_infix'))) 
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

107 
>> (Toplevel.theory o Theory.add_tyabbrs o 
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

108 
map (fn ((args, a), (T, mx)) => (a, args, T, mx)))); 
5832  109 

110 
val nontermP = 

6370  111 
OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols" 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

112 
K.thy_decl (Scan.repeat1 P.name >> (Toplevel.theory o Theory.add_nonterminals)); 
5832  113 

114 
val aritiesP = 

6723  115 
OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

116 
(Scan.repeat1 (P.xname  (P.$$$ "::"  P.!!! P.arity) >> P.triple2) 
19516  117 
>> (Toplevel.theory o fold AxClass.axiomatize_arity)); 
5832  118 

119 

120 
(* consts and syntax *) 

121 

8227  122 
val judgmentP = 
123 
OuterSyntax.command "judgment" "declare objectlogic judgment" K.thy_decl 

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

124 
(P.const >> (Toplevel.theory o ObjectLogic.add_judgment)); 
8227  125 

5832  126 
val constsP = 
6723  127 
OuterSyntax.command "consts" "declare constants" K.thy_decl 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

128 
(Scan.repeat1 P.const >> (Toplevel.theory o Theory.add_consts)); 
5832  129 

14642  130 
val opt_overloaded = P.opt_keyword "overloaded"; 
14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
13802
diff
changeset

131 

0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
13802
diff
changeset

132 
val finalconstsP = 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
13802
diff
changeset

133 
OuterSyntax.command "finalconsts" "declare constants as final" K.thy_decl 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
13802
diff
changeset

134 
(opt_overloaded  Scan.repeat1 P.term >> (uncurry (Toplevel.theory oo Theory.add_finals))); 
9731  135 

12142  136 
val mode_spec = 
9731  137 
(P.$$$ "output" >> K ("", false))  P.name  Scan.optional (P.$$$ "output" >> K false) true; 
138 

14900  139 
val opt_mode = 
140 
Scan.optional (P.$$$ "("  P.!!! (mode_spec  P.$$$ ")")) Syntax.default_mode; 

5832  141 

142 
val syntaxP = 

6723  143 
OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

144 
(opt_mode  Scan.repeat1 P.const >> (Toplevel.theory o uncurry Theory.add_modesyntax)); 
5832  145 

15748  146 
val no_syntaxP = 
147 
OuterSyntax.command "no_syntax" "delete syntax declarations" K.thy_decl 

148 
(opt_mode  Scan.repeat1 P.const >> (Toplevel.theory o uncurry Theory.del_modesyntax)); 

149 

5832  150 

151 
(* translations *) 

152 

153 
val trans_pat = 

6723  154 
Scan.optional (P.$$$ "("  P.!!! (P.xname  P.$$$ ")")) "logic"  P.string; 
5832  155 

156 
fun trans_arrow toks = 

10688  157 
((P.$$$ "\\<rightharpoonup>"  P.$$$ "=>") >> K Syntax.ParseRule  
158 
(P.$$$ "\\<leftharpoondown>"  P.$$$ "<=") >> K Syntax.PrintRule  

159 
(P.$$$ "\\<rightleftharpoons>"  P.$$$ "==") >> K Syntax.ParsePrintRule) toks; 

5832  160 

161 
val trans_line = 

6723  162 
trans_pat  P.!!! (trans_arrow  trans_pat) 
5832  163 
>> (fn (left, (arr, right)) => arr (left, right)); 
164 

165 
val translationsP = 

6723  166 
OuterSyntax.command "translations" "declare syntax translation rules" K.thy_decl 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

167 
(Scan.repeat1 trans_line >> (Toplevel.theory o Theory.add_trrules)); 
5832  168 

19260  169 
val no_translationsP = 
170 
OuterSyntax.command "no_translations" "remove syntax translation rules" K.thy_decl 

171 
(Scan.repeat1 trans_line >> (Toplevel.theory o Theory.del_trrules)); 

172 

5832  173 

174 
(* axioms and definitions *) 

175 

176 
val axiomsP = 

6723  177 
OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl 
22117  178 
(Scan.repeat1 SpecParse.spec_name >> (Toplevel.theory o IsarCmd.add_axioms)); 
5832  179 

19631  180 
val opt_unchecked_overloaded = 
181 
Scan.optional (P.$$$ "("  P.!!! 

182 
(((P.$$$ "unchecked" >> K true)  Scan.optional (P.$$$ "overloaded" >> K true) false  

183 
P.$$$ "overloaded" >> K (false, true))  P.$$$ ")")) (false, false); 

184 

5832  185 
val defsP = 
6723  186 
OuterSyntax.command "defs" "define constants" K.thy_decl 
22117  187 
(opt_unchecked_overloaded  Scan.repeat1 SpecParse.spec_name 
21350  188 
>> (Toplevel.theory o IsarCmd.add_defs)); 
6370  189 

14642  190 

21601
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

191 
(* old constdefs *) 
14642  192 

21601
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

193 
val old_constdecl = 
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

194 
P.name  P.where_ >> (fn x => (x, NONE, NoSyn))  
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

195 
P.name  (P.$$$ "::"  P.!!! P.typ >> SOME)  P.opt_mixfix' 
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

196 
 Scan.option P.where_ >> P.triple1  
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

197 
P.name  (P.mixfix >> pair NONE)  Scan.option P.where_ >> P.triple2; 
19076  198 

22117  199 
val old_constdef = Scan.option old_constdecl  (SpecParse.opt_thm_name ":"  P.prop); 
14642  200 

19076  201 
val structs = 
202 
Scan.optional ((P.$$$ "("  P.$$$ "structure")  P.!!! (P.simple_fixes  P.$$$ ")")) []; 

203 

6370  204 
val constdefsP = 
19076  205 
OuterSyntax.command "constdefs" "oldstyle constant definition" K.thy_decl 
21601
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

206 
(structs  Scan.repeat1 old_constdef >> (Toplevel.theory o Constdefs.add_constdefs)); 
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

207 

6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

208 

6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

209 
(* constant definitions and abbreviations *) 
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

210 

6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

211 
val constdecl = 
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

212 
P.name  
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

213 
(P.where_ >> K (NONE, NoSyn)  
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

214 
P.$$$ "::"  P.!!! ((P.typ >> SOME)  P.opt_mixfix'  P.where_)  
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

215 
Scan.ahead (P.$$$ "(")  P.!!! (P.mixfix'  P.where_ >> pair NONE)) 
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

216 
>> P.triple2; 
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

217 

22117  218 
val constdef = Scan.option constdecl  (SpecParse.opt_thm_name ":"  P.prop); 
5832  219 

18780  220 
val definitionP = 
19076  221 
OuterSyntax.command "definition" "constant definition" K.thy_decl 
22117  222 
(P.opt_target  constdef 
18949  223 
>> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.definition args))); 
18780  224 

19076  225 
val abbreviationP = 
226 
OuterSyntax.command "abbreviation" "constant abbreviation" K.thy_decl 

22117  227 
(P.opt_target  opt_mode  (Scan.option constdecl  P.prop) 
19659  228 
>> (fn ((loc, mode), args) => 
21527  229 
Toplevel.local_theory loc (Specification.abbreviation mode args))); 
19659  230 

21210  231 
val notationP = 
232 
OuterSyntax.command "notation" "variable/constant syntax" K.thy_decl 

22117  233 
(P.opt_target  opt_mode  P.and_list1 (P.xname  P.mixfix) 
19659  234 
>> (fn ((loc, mode), args) => 
21210  235 
Toplevel.local_theory loc (Specification.notation mode args))); 
19076  236 

5832  237 

18616  238 
(* constant specifications *) 
239 

240 
val axiomatizationP = 

241 
OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl 

22117  242 
(P.opt_target  
18949  243 
(Scan.optional P.fixes []  
22117  244 
Scan.optional (P.where_  P.!!! (P.and_list1 SpecParse.spec)) []) 
18949  245 
>> (fn (loc, (x, y)) => Toplevel.local_theory loc (#2 o Specification.axiomatization x y))); 
18616  246 

247 

5914  248 
(* theorems *) 
249 

22117  250 
fun theorems kind = P.opt_target  SpecParse.name_facts 
20907  251 
>> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.theorems kind args)); 
12712  252 

5914  253 
val theoremsP = 
21437  254 
OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK); 
5914  255 

256 
val lemmasP = 

21437  257 
OuterSyntax.command "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK); 
5914  258 

9589  259 
val declareP = 
9776  260 
OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script 
22117  261 
(P.opt_target  (P.and_list1 SpecParse.xthms1 >> flat) 
20907  262 
>> (fn (loc, args) => Toplevel.local_theory loc 
263 
(#2 o Specification.theorems "" [(("", []), args)]))); 

9589  264 

5914  265 

5832  266 
(* name space entry path *) 
267 

268 
val globalP = 

6723  269 
OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl 
16447  270 
(Scan.succeed (Toplevel.theory Sign.root_path)); 
5832  271 

272 
val localP = 

6723  273 
OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl 
16447  274 
(Scan.succeed (Toplevel.theory Sign.local_path)); 
8723  275 

276 
val hideP = 

277 
OuterSyntax.command "hide" "hide names from given name space" K.thy_decl 

17397  278 
((P.opt_keyword "open" >> not)  (P.name  Scan.repeat1 P.xname) >> 
279 
(Toplevel.theory o uncurry Sign.hide_names)); 

5832  280 

281 

282 
(* use ML text *) 

283 

284 
val useP = 

17068  285 
OuterSyntax.command "use" "eval ML text from file" (K.tag_ml K.diag) 
14950  286 
(P.path >> (Toplevel.no_timing oo IsarCmd.use)); 
5832  287 

288 
val mlP = 

17068  289 
OuterSyntax.command "ML" "eval ML text (diagnostic)" (K.tag_ml K.diag) 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

290 
(P.text >> IsarCmd.use_mltext true); 
7891  291 

292 
val ml_commandP = 

17068  293 
OuterSyntax.command "ML_command" "eval ML text" (K.tag_ml K.diag) 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

294 
(P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false)); 
7616  295 

296 
val ml_setupP = 

17068  297 
OuterSyntax.command "ML_setup" "eval ML text (may change theory)" (K.tag_ml K.thy_decl) 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

298 
(P.text >> IsarCmd.use_mltext_theory); 
5832  299 

300 
val setupP = 

17068  301 
OuterSyntax.command "setup" "apply ML theory setup" (K.tag_ml K.thy_decl) 
22117  302 
(Scan.option P.text >> (Toplevel.theory o IsarCmd.generic_setup)); 
5832  303 

9197  304 
val method_setupP = 
17068  305 
OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl) 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

306 
(((P.name  P.!!! (P.$$$ "="  P.text  P.text) >> P.triple2)) 
17353  307 
>> (Toplevel.theory o Method.method_setup)); 
9197  308 

22088  309 
val declarationP = 
310 
OuterSyntax.command "declaration" "generic ML declaration" (K.tag_ml K.thy_decl) 

22117  311 
(P.opt_target  P.text 
22088  312 
>> (fn (loc, txt) => Toplevel.local_theory loc (IsarCmd.declaration txt))); 
313 

5832  314 

315 
(* translation functions *) 

316 

14642  317 
val trfun = P.opt_keyword "advanced"  P.text; 
318 

5832  319 
val parse_ast_translationP = 
17068  320 
OuterSyntax.command "parse_ast_translation" "install parse ast translation functions" 
321 
(K.tag_ml K.thy_decl) 

22117  322 
(trfun >> (Toplevel.theory o IsarCmd.parse_ast_translation)); 
5832  323 

324 
val parse_translationP = 

17068  325 
OuterSyntax.command "parse_translation" "install parse translation functions" 
326 
(K.tag_ml K.thy_decl) 

22117  327 
(trfun >> (Toplevel.theory o IsarCmd.parse_translation)); 
5832  328 

329 
val print_translationP = 

17068  330 
OuterSyntax.command "print_translation" "install print translation functions" 
331 
(K.tag_ml K.thy_decl) 

22117  332 
(trfun >> (Toplevel.theory o IsarCmd.print_translation)); 
5832  333 

334 
val typed_print_translationP = 

6370  335 
OuterSyntax.command "typed_print_translation" "install typed print translation functions" 
17068  336 
(K.tag_ml K.thy_decl) 
22117  337 
(trfun >> (Toplevel.theory o IsarCmd.typed_print_translation)); 
5832  338 

339 
val print_ast_translationP = 

17068  340 
OuterSyntax.command "print_ast_translation" "install print ast translation functions" 
341 
(K.tag_ml K.thy_decl) 

22117  342 
(trfun >> (Toplevel.theory o IsarCmd.print_ast_translation)); 
5832  343 

344 
val token_translationP = 

17068  345 
OuterSyntax.command "token_translation" "install token translation functions" 
346 
(K.tag_ml K.thy_decl) 

22117  347 
(P.text >> (Toplevel.theory o IsarCmd.token_translation)); 
5832  348 

349 

350 
(* oracles *) 

351 

352 
val oracleP = 

17068  353 
OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl) 
16849  354 
(P.name  (P.$$$ "("  P.text  P.$$$ ")"  P.$$$ "=") 
22117  355 
 P.text >> (Toplevel.theory o IsarCmd.oracle o P.triple1)); 
5832  356 

357 

21306
7ab6e95e6b0b
turned 'context' into plain thy_decl, discontinued thy_switch;
wenzelm
parents:
21269
diff
changeset

358 
(* local theories *) 
7ab6e95e6b0b
turned 'context' into plain thy_decl, discontinued thy_switch;
wenzelm
parents:
21269
diff
changeset

359 

7ab6e95e6b0b
turned 'context' into plain thy_decl, discontinued thy_switch;
wenzelm
parents:
21269
diff
changeset

360 
val contextP = 
7ab6e95e6b0b
turned 'context' into plain thy_decl, discontinued thy_switch;
wenzelm
parents:
21269
diff
changeset

361 
OuterSyntax.command "context" "enter local theory context" K.thy_decl 
7ab6e95e6b0b
turned 'context' into plain thy_decl, discontinued thy_switch;
wenzelm
parents:
21269
diff
changeset

362 
(P.name  P.begin >> (fn name => 
7ab6e95e6b0b
turned 'context' into plain thy_decl, discontinued thy_switch;
wenzelm
parents:
21269
diff
changeset

363 
Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.init (SOME name)))); 
7ab6e95e6b0b
turned 'context' into plain thy_decl, discontinued thy_switch;
wenzelm
parents:
21269
diff
changeset

364 

7ab6e95e6b0b
turned 'context' into plain thy_decl, discontinued thy_switch;
wenzelm
parents:
21269
diff
changeset

365 

12061  366 
(* locales *) 
367 

12758  368 
val locale_val = 
22117  369 
(SpecParse.locale_expr  
370 
Scan.optional (P.$$$ "+"  P.!!! (Scan.repeat1 SpecParse.context_element)) []  

371 
Scan.repeat1 SpecParse.context_element >> pair Locale.empty); 

12061  372 

373 
val localeP = 

374 
OuterSyntax.command "locale" "define named proof context" K.thy_decl 

14642  375 
((P.opt_keyword "open" >> not)  P.name 
376 
 Scan.optional (P.$$$ "="  P.!!! locale_val) (Locale.empty, []) 

20958  377 
 P.opt_begin 
378 
>> (fn (((is_open, name), (expr, elems)), begin) => 

21843  379 
(begin ? Toplevel.print) o Toplevel.begin_local_theory begin 
21800
6035bfcd72d8
classified show/thus as prf_asm_goal, which is usually hilited in PG;
wenzelm
parents:
21726
diff
changeset

380 
(Locale.add_locale is_open name expr elems #> TheoryTarget.begin false))); 
12061  381 

15598
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset

382 
val interpretationP = 
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset

383 
OuterSyntax.command "interpretation" 
16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16604
diff
changeset

384 
"prove and register interpretation of locale expression in theory or locale" K.thy_goal 
22117  385 
(P.xname  (P.$$$ "\\<subseteq>"  P.$$$ "<")  P.!!! SpecParse.locale_expr 
20365  386 
>> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I))  
22117  387 
SpecParse.opt_thm_name ":"  SpecParse.locale_expr  SpecParse.locale_insts >> (fn ((x, y), z) => 
20365  388 
Toplevel.print o Toplevel.theory_to_proof (Locale.interpretation I x y z))); 
12061  389 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

390 
val interpretP = 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

391 
OuterSyntax.command "interpret" 
17068  392 
"prove and register interpretation of locale expression in proof context" 
393 
(K.tag_proof K.prf_goal) 

22117  394 
(SpecParse.opt_thm_name ":"  SpecParse.locale_expr  SpecParse.locale_insts 
395 
>> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Locale.interpret Seq.single x y z))); 

15703  396 

397 

5832  398 

399 
(** proof commands **) 

400 

401 
(* statements *) 

402 

17353  403 
fun gen_theorem kind = 
404 
OuterSyntax.command kind ("state " ^ kind) K.thy_goal 

22117  405 
(P.opt_target  Scan.optional (SpecParse.opt_thm_name ":"  
406 
Scan.ahead (SpecParse.locale_keyword  SpecParse.statement_keyword)) ("", [])  

407 
SpecParse.general_statement >> (fn ((loc, a), (elems, concl)) => 

21033  408 
(Toplevel.print o 
409 
Toplevel.local_theory_to_proof loc 

21228  410 
(Specification.theorem kind NONE (K I) a elems concl)))); 
5832  411 

21437  412 
val theoremP = gen_theorem Thm.theoremK; 
413 
val lemmaP = gen_theorem Thm.lemmaK; 

414 
val corollaryP = gen_theorem Thm.corollaryK; 

5832  415 

17353  416 
val haveP = 
417 
OuterSyntax.command "have" "state local goal" 

418 
(K.tag_proof K.prf_goal) 

22117  419 
(SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have)); 
17353  420 

421 
val henceP = 

422 
OuterSyntax.command "hence" "abbreviates \"then have\"" 

423 
(K.tag_proof K.prf_goal) 

22117  424 
(SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence)); 
17353  425 

5832  426 
val showP = 
17068  427 
OuterSyntax.command "show" "state local goal, solving current obligation" 
21800
6035bfcd72d8
classified show/thus as prf_asm_goal, which is usually hilited in PG;
wenzelm
parents:
21726
diff
changeset

428 
(K.tag_proof K.prf_asm_goal) 
22117  429 
(SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show)); 
5832  430 

6501  431 
val thusP = 
17068  432 
OuterSyntax.command "thus" "abbreviates \"then show\"" 
21800
6035bfcd72d8
classified show/thus as prf_asm_goal, which is usually hilited in PG;
wenzelm
parents:
21726
diff
changeset

433 
(K.tag_proof K.prf_asm_goal) 
22117  434 
(SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus)); 
6501  435 

5832  436 

5914  437 
(* facts *) 
5832  438 

22117  439 
val facts = P.and_list1 SpecParse.xthms1; 
9197  440 

5832  441 
val thenP = 
17068  442 
OuterSyntax.command "then" "forward chaining" 
443 
(K.tag_proof K.prf_chain) 

17900  444 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain)); 
5832  445 

446 
val fromP = 

17068  447 
OuterSyntax.command "from" "forward chaining from given facts" 
448 
(K.tag_proof K.prf_chain) 

17900  449 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss))); 
5914  450 

6878  451 
val withP = 
17068  452 
OuterSyntax.command "with" "forward chaining from given and current facts" 
453 
(K.tag_proof K.prf_chain) 

17900  454 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss))); 
6878  455 

6773  456 
val noteP = 
17068  457 
OuterSyntax.command "note" "define facts" 
458 
(K.tag_proof K.prf_decl) 

22117  459 
(SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss))); 
5832  460 

12926  461 
val usingP = 
17068  462 
OuterSyntax.command "using" "augment goal facts" 
463 
(K.tag_proof K.prf_decl) 

18544  464 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.using))); 
465 

466 
val unfoldingP = 

467 
OuterSyntax.command "unfolding" "unfold definitions in goal and facts" 

468 
(K.tag_proof K.prf_decl) 

469 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding))); 

12926  470 

5832  471 

472 
(* proof context *) 

473 

11890  474 
val fixP = 
17068  475 
OuterSyntax.command "fix" "fix local variables (Skolem constants)" 
476 
(K.tag_proof K.prf_asm) 

19844  477 
(P.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix))); 
11890  478 

5832  479 
val assumeP = 
17068  480 
OuterSyntax.command "assume" "assume propositions" 
481 
(K.tag_proof K.prf_asm) 

22117  482 
(SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume))); 
5832  483 

6850  484 
val presumeP = 
17068  485 
OuterSyntax.command "presume" "assume propositions, to be established later" 
486 
(K.tag_proof K.prf_asm) 

22117  487 
(SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume))); 
6850  488 

6953  489 
val defP = 
17068  490 
OuterSyntax.command "def" "local definition" 
491 
(K.tag_proof K.prf_asm) 

18308  492 
(P.and_list1 
22117  493 
(SpecParse.opt_thm_name ":"  
19844  494 
((P.name  P.opt_mixfix)  ((P.$$$ "\\<equiv>"  P.$$$ "==")  P.!!! P.termp))) 
18308  495 
>> (Toplevel.print oo (Toplevel.proof o Proof.def))); 
6953  496 

11890  497 
val obtainP = 
498 
OuterSyntax.command "obtain" "generalized existence" 

17068  499 
(K.tag_proof K.prf_asm_goal) 
22117  500 
(P.parname  Scan.optional (P.fixes  P.where_) []  SpecParse.statement 
18895  501 
>> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain x y z))); 
5832  502 

17854  503 
val guessP = 
504 
OuterSyntax.command "guess" "wild guessing (unstructured)" 

505 
(K.tag_proof K.prf_asm_goal) 

19844  506 
(Scan.optional P.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess))); 
17854  507 

5832  508 
val letP = 
17068  509 
OuterSyntax.command "let" "bind text variables" 
510 
(K.tag_proof K.prf_decl) 

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

511 
(P.and_list1 (P.enum1 "and" P.term  (P.$$$ "="  P.term)) 
17900  512 
>> (Toplevel.print oo (Toplevel.proof o Proof.let_bind))); 
5832  513 

11793
5f0ab6f5c280
support impromptu terminology of cases parameters;
wenzelm
parents:
11742
diff
changeset

514 
val case_spec = 
15703  515 
(P.$$$ "("  P.!!! (P.xname  Scan.repeat1 (P.maybe P.name)  P.$$$ ")")  
22117  516 
P.xname >> rpair [])  SpecParse.opt_attribs >> P.triple1; 
11793
5f0ab6f5c280
support impromptu terminology of cases parameters;
wenzelm
parents:
11742
diff
changeset

517 

8370  518 
val caseP = 
17068  519 
OuterSyntax.command "case" "invoke local context" 
520 
(K.tag_proof K.prf_asm) 

17900  521 
(case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case))); 
8370  522 

5832  523 

524 
(* proof structure *) 

525 

20958  526 
val begin_blockP = 
17068  527 
OuterSyntax.command "{" "begin explicit proof block" 
528 
(K.tag_proof K.prf_open) 

17900  529 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block)); 
5832  530 

20958  531 
val end_blockP = 
17068  532 
OuterSyntax.command "}" "end explicit proof block" 
533 
(K.tag_proof K.prf_close) 

20305  534 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block)); 
6687  535 

5832  536 
val nextP = 
17068  537 
OuterSyntax.command "next" "enter next proof block" 
538 
(K.tag_proof K.prf_block) 

17900  539 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block)); 
5832  540 

541 

542 
(* end proof *) 

543 

6404  544 
val qedP = 
17068  545 
OuterSyntax.command "qed" "conclude (sub)proof" 
546 
(K.tag_proof K.qed_block) 

22117  547 
(Scan.option Method.parse >> (Toplevel.print3 oo IsarCmd.qed)); 
5832  548 

6404  549 
val terminal_proofP = 
17068  550 
OuterSyntax.command "by" "terminal backward proof" 
551 
(K.tag_proof K.qed) 

22117  552 
(Method.parse  Scan.option Method.parse >> (Toplevel.print3 oo IsarCmd.terminal_proof)); 
6404  553 

8966  554 
val default_proofP = 
17068  555 
OuterSyntax.command ".." "default proof" 
556 
(K.tag_proof K.qed) 

21350  557 
(Scan.succeed (Toplevel.print3 o IsarCmd.default_proof)); 
8966  558 

6404  559 
val immediate_proofP = 
17068  560 
OuterSyntax.command "." "immediate proof" 
561 
(K.tag_proof K.qed) 

21350  562 
(Scan.succeed (Toplevel.print3 o IsarCmd.immediate_proof)); 
6404  563 

8966  564 
val done_proofP = 
17068  565 
OuterSyntax.command "done" "done proof" 
566 
(K.tag_proof K.qed) 

21350  567 
(Scan.succeed (Toplevel.print3 o IsarCmd.done_proof)); 
5832  568 

6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
6886
diff
changeset

569 
val skip_proofP = 
17068  570 
OuterSyntax.improper_command "sorry" "skip proof (quickanddirty mode only!)" 
571 
(K.tag_proof K.qed) 

21350  572 
(Scan.succeed (Toplevel.print3 o IsarCmd.skip_proof)); 
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
6886
diff
changeset

573 

8210  574 
val forget_proofP = 
17068  575 
OuterSyntax.command "oops" "forget proof" 
576 
(K.tag_proof K.qed_global) 

18561  577 
(Scan.succeed Toplevel.forget_proof); 
8210  578 

5832  579 

580 
(* proof steps *) 

581 

8165  582 
val deferP = 
17068  583 
OuterSyntax.command "defer" "shuffle internal proof state" 
584 
(K.tag_proof K.prf_script) 

17900  585 
(Scan.option P.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer))); 
8165  586 

587 
val preferP = 

17068  588 
OuterSyntax.command "prefer" "shuffle internal proof state" 
589 
(K.tag_proof K.prf_script) 

17900  590 
(P.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.prefer))); 
8165  591 

6850  592 
val applyP = 
17068  593 
OuterSyntax.command "apply" "initial refinement step (unstructured)" 
594 
(K.tag_proof K.prf_script) 

22117  595 
(Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply))); 
5832  596 

8235  597 
val apply_endP = 
17068  598 
OuterSyntax.command "apply_end" "terminal refinement (unstructured)" 
599 
(K.tag_proof K.prf_script) 

22117  600 
(Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end))); 
5832  601 

6404  602 
val proofP = 
17068  603 
OuterSyntax.command "proof" "backward proof" 
604 
(K.tag_proof K.prf_block) 

22117  605 
(Scan.option Method.parse >> (fn m => Toplevel.print o 
17107
2c35e00ee2ab
various Toplevel.theory_context commands: proper presentation in context;
wenzelm
parents:
17068
diff
changeset

606 
Toplevel.actual_proof (ProofHistory.applys (Proof.proof m)) o 
15237
250e9be7a09d
Some changes to allow skipping of proof scripts.
berghofe
parents:
15141
diff
changeset

607 
Toplevel.skip_proof (History.apply (fn i => i + 1)))); 
5832  608 

609 

6773  610 
(* calculational proof commands *) 
611 

6878  612 
val calc_args = 
22117  613 
Scan.option (P.$$$ "("  P.!!! ((SpecParse.xthms1  P.$$$ ")"))); 
6878  614 

6773  615 
val alsoP = 
17068  616 
OuterSyntax.command "also" "combine calculation and current facts" 
617 
(K.tag_proof K.prf_decl) 

17900  618 
(calc_args >> (Toplevel.proofs' o Calculation.also)); 
6773  619 

620 
val finallyP = 

17068  621 
OuterSyntax.command "finally" "combine calculation and current facts, exhibit result" 
622 
(K.tag_proof K.prf_chain) 

17900  623 
(calc_args >> (Toplevel.proofs' o Calculation.finally)); 
6773  624 

8562  625 
val moreoverP = 
17068  626 
OuterSyntax.command "moreover" "augment calculation by current facts" 
627 
(K.tag_proof K.prf_decl) 

17900  628 
(Scan.succeed (Toplevel.proof' Calculation.moreover)); 
8562  629 

8588  630 
val ultimatelyP = 
631 
OuterSyntax.command "ultimately" "augment calculation by current facts, exhibit result" 

17068  632 
(K.tag_proof K.prf_chain) 
17900  633 
(Scan.succeed (Toplevel.proof' Calculation.ultimately)); 
8588  634 

6773  635 

6742  636 
(* proof navigation *) 
5944  637 

5832  638 
val backP = 
17068  639 
OuterSyntax.command "back" "backtracking of proof command" 
640 
(K.tag_proof K.prf_script) 

641 
(Scan.succeed (Toplevel.print o IsarCmd.back)); 

5832  642 

643 

6742  644 
(* history *) 
645 

20979  646 
val cannot_undoP = 
647 
OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control 

648 
(P.name >> (Toplevel.no_timing oo IsarCmd.cannot_undo)); 

6742  649 

650 
val redoP = 

651 
OuterSyntax.improper_command "redo" "redo last command" K.control 

9010  652 
(Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.redo)); 
6742  653 

654 
val undos_proofP = 

655 
OuterSyntax.improper_command "undos_proof" "undo last proof commands" K.control 

9010  656 
(P.nat >> ((Toplevel.no_timing o Toplevel.print) oo IsarCmd.undos_proof)); 
6742  657 

658 
val undoP = 

659 
OuterSyntax.improper_command "undo" "undo last command" K.control 

9010  660 
(Scan.succeed ((Toplevel.no_timing o Toplevel.print) o IsarCmd.undo)); 
6742  661 

8500  662 
val killP = 
663 
OuterSyntax.improper_command "kill" "kill current history node" K.control 

9010  664 
(Scan.succeed ((Toplevel.no_timing o Toplevel.print) o IsarCmd.kill)); 
8500  665 

6742  666 

5832  667 

668 
(** diagnostic commands (for interactive mode only) **) 

669 

8464  670 
val opt_modes = Scan.optional (P.$$$ "("  P.!!! (Scan.repeat1 P.xname  P.$$$ ")")) []; 
20621  671 
val opt_bang = Scan.optional (P.$$$ "!" >> K true) false; 
8464  672 

7124  673 
val pretty_setmarginP = 
674 
OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing" 

9010  675 
K.diag (P.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin)); 
7124  676 

21714  677 
val helpP = 
678 
OuterSyntax.improper_command "help" "print outer syntax commands" K.diag 

679 
(Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands)); 

680 

5832  681 
val print_commandsP = 
21714  682 
OuterSyntax.improper_command "print_commands" "print outer syntax commands" K.diag 
9221  683 
(Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands)); 
5832  684 

7308  685 
val print_contextP = 
686 
OuterSyntax.improper_command "print_context" "print theory context name" K.diag 

9010  687 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_context)); 
7308  688 

5832  689 
val print_theoryP = 
6723  690 
OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag 
20621  691 
(opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory)); 
5832  692 

693 
val print_syntaxP = 

21726  694 
OuterSyntax.improper_command "print_syntax" "print inner syntax of context (verbose!)" K.diag 
9010  695 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax)); 
5832  696 

21726  697 
val print_abbrevsP = 
698 
OuterSyntax.improper_command "print_abbrevs" "print constant abbreviation of context" K.diag 

699 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_abbrevs)); 

700 

5881  701 
val print_theoremsP = 
17068  702 
OuterSyntax.improper_command "print_theorems" 
703 
"print theorems of local theory or proof context" K.diag 

9010  704 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_theorems)); 
5881  705 

12061  706 
val print_localesP = 
707 
OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag 

708 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_locales)); 

709 

710 
val print_localeP = 

15596  711 
OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag 
20621  712 
(opt_bang  locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale)); 
12061  713 

15596  714 
val print_registrationsP = 
15598
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset

715 
OuterSyntax.improper_command "print_interps" 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16074
diff
changeset

716 
"print interpretations of named locale" K.diag 
18670  717 
(Scan.optional (P.$$$ "!" >> K true) false  P.xname 
718 
>> (Toplevel.no_timing oo uncurry IsarCmd.print_registrations)); 

15596  719 

5832  720 
val print_attributesP = 
12061  721 
OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag 
9010  722 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes)); 
5832  723 

16027  724 
val print_simpsetP = 
725 
OuterSyntax.improper_command "print_simpset" "print context of Simplifier" K.diag 

726 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_simpset)); 

727 

12383  728 
val print_rulesP = 
729 
OuterSyntax.improper_command "print_rules" "print intro/elim rules" K.diag 

730 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_rules)); 

731 

11666  732 
val print_induct_rulesP = 
733 
OuterSyntax.improper_command "print_induct_rules" "print induction and cases rules" K.diag 

734 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_induct_rules)); 

735 

9221  736 
val print_trans_rulesP = 
11666  737 
OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" K.diag 
9221  738 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules)); 
739 

5832  740 
val print_methodsP = 
12061  741 
OuterSyntax.improper_command "print_methods" "print methods of this theory" K.diag 
9010  742 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods)); 
5832  743 

9221  744 
val print_antiquotationsP = 
745 
OuterSyntax.improper_command "print_antiquotations" "print antiquotations (global)" K.diag 

746 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations)); 

747 

20574  748 
val class_depsP = 
749 
OuterSyntax.improper_command "class_deps" "visualize class dependencies" 

750 
K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps)); 

751 

9454  752 
val thm_depsP = 
753 
OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies" 

22117  754 
K.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps)); 
9454  755 

16027  756 
val criterion = 
757 
P.reserved "name"  P.!!! (P.$$$ ":"  P.xname) >> FindTheorems.Name  

758 
P.reserved "intro" >> K FindTheorems.Intro  

759 
P.reserved "elim" >> K FindTheorems.Elim  

760 
P.reserved "dest" >> K FindTheorems.Dest  

16074  761 
P.reserved "simp"  P.!!! (P.$$$ ":"  P.term) >> FindTheorems.Simp  
16027  762 
P.term >> FindTheorems.Pattern; 
763 

764 
val find_theoremsP = 

17219
515badbfc4d6
renamed 'thms_containing' to 'find_theorems'  keep old version for the time being;
wenzelm
parents:
17142
diff
changeset

765 
OuterSyntax.improper_command "find_theorems" 
515badbfc4d6
renamed 'thms_containing' to 'find_theorems'  keep old version for the time being;
wenzelm
parents:
17142
diff
changeset

766 
"print theorems meeting specified criteria" K.diag 
515badbfc4d6
renamed 'thms_containing' to 'find_theorems'  keep old version for the time being;
wenzelm
parents:
17142
diff
changeset

767 
(Scan.option (P.$$$ "("  P.!!! (P.nat  P.$$$ ")"))  
515badbfc4d6
renamed 'thms_containing' to 'find_theorems'  keep old version for the time being;
wenzelm
parents:
17142
diff
changeset

768 
Scan.repeat (((Scan.option P.minus >> is_none)  criterion)) 
515badbfc4d6
renamed 'thms_containing' to 'find_theorems'  keep old version for the time being;
wenzelm
parents:
17142
diff
changeset

769 
>> (Toplevel.no_timing oo IsarCmd.find_theorems)); 
515badbfc4d6
renamed 'thms_containing' to 'find_theorems'  keep old version for the time being;
wenzelm
parents:
17142
diff
changeset

770 

5832  771 
val print_bindsP = 
6723  772 
OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag 
9010  773 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds)); 
5832  774 

21004  775 
val print_factsP = 
8370  776 
OuterSyntax.improper_command "print_facts" "print facts of proof context" K.diag 
21004  777 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_facts)); 
5832  778 

8370  779 
val print_casesP = 
780 
OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag 

9010  781 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases)); 
8370  782 

19269  783 
val print_stmtsP = 
784 
OuterSyntax.improper_command "print_statement" "print theorems as long statements" K.diag 

22117  785 
(opt_modes  SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts)); 
19269  786 

5896  787 
val print_thmsP = 
8464  788 
OuterSyntax.improper_command "thm" "print theorems" K.diag 
22117  789 
(opt_modes  SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms)); 
5832  790 

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

791 
val print_prfsP = 
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11101
diff
changeset

792 
OuterSyntax.improper_command "prf" "print proof terms of theorems" K.diag 
22117  793 
(opt_modes  Scan.option SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs false)); 
11524
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11101
diff
changeset

794 

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

795 
val print_full_prfsP = 
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11101
diff
changeset

796 
OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" K.diag 
22117  797 
(opt_modes  Scan.option SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true)); 
11524
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11101
diff
changeset

798 

5832  799 
val print_propP = 
6723  800 
OuterSyntax.improper_command "prop" "read and print proposition" K.diag 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

801 
(opt_modes  P.term >> (Toplevel.no_timing oo IsarCmd.print_prop)); 
5832  802 

803 
val print_termP = 

6723  804 
OuterSyntax.improper_command "term" "read and print term" K.diag 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

805 
(opt_modes  P.term >> (Toplevel.no_timing oo IsarCmd.print_term)); 
5832  806 

807 
val print_typeP = 

6723  808 
OuterSyntax.improper_command "typ" "read and print type" K.diag 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

809 
(opt_modes  P.typ >> (Toplevel.no_timing oo IsarCmd.print_type)); 
5832  810 

811 

812 

813 
(** system commands (for interactive mode only) **) 

814 

815 
val cdP = 

8650  816 
OuterSyntax.improper_command "cd" "change current working directory" K.diag 
14950  817 
(P.path >> (Toplevel.no_timing oo IsarCmd.cd)); 
5832  818 

819 
val pwdP = 

6723  820 
OuterSyntax.improper_command "pwd" "print current working directory" K.diag 
9010  821 
(Scan.succeed (Toplevel.no_timing o IsarCmd.pwd)); 
5832  822 

823 
val use_thyP = 

6723  824 
OuterSyntax.improper_command "use_thy" "use theory file" K.diag 
9010  825 
(P.name >> (Toplevel.no_timing oo IsarCmd.use_thy)); 
5832  826 

6694  827 
val use_thy_onlyP = 
7102  828 
OuterSyntax.improper_command "use_thy_only" "use theory file only, ignoring associated ML" 
9010  829 
K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy_only)); 
6694  830 

6196  831 
val update_thyP = 
6723  832 
OuterSyntax.improper_command "update_thy" "update theory file" K.diag 
9010  833 
(P.name >> (Toplevel.no_timing oo IsarCmd.update_thy)); 
5832  834 

7102  835 
val update_thy_onlyP = 
836 
OuterSyntax.improper_command "update_thy_only" "update theory file, ignoring associated ML" 

9010  837 
K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.update_thy_only)); 
7102  838 

839 
val touch_thyP = 

840 
OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag 

9010  841 
(P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy)); 
7102  842 

843 
val touch_all_thysP = 

844 
OuterSyntax.improper_command "touch_all_thys" "outdate all nonfinished theories" K.diag 

9010  845 
(Scan.succeed (Toplevel.no_timing o IsarCmd.touch_all_thys)); 
7102  846 

7908  847 
val touch_child_thysP = 
848 
OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag 

9010  849 
(P.name >> (Toplevel.no_timing oo IsarCmd.touch_child_thys)); 
7908  850 

7102  851 
val remove_thyP = 
852 
OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag 

9010  853 
(P.name >> (Toplevel.no_timing oo IsarCmd.remove_thy)); 
7102  854 

7931  855 
val kill_thyP = 
856 
OuterSyntax.improper_command "kill_thy" "kill theory  try to remove from loader database" 

9010  857 
K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.kill_thy)); 
7931  858 

14934  859 
val display_draftsP = 
860 
OuterSyntax.improper_command "display_drafts" "display raw source files with symbols" 

14950  861 
K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.display_drafts)); 
14934  862 

863 
val print_draftsP = 

864 
OuterSyntax.improper_command "print_drafts" "print raw source files with symbols" 

14950  865 
K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.print_drafts)); 
14934  866 

9731  867 
val opt_limits = 
868 
Scan.option P.nat  Scan.option (P.$$$ ","  P.!!! P.nat); 

869 

5832  870 
val prP = 
8886  871 
OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag 
9731  872 
(opt_modes  opt_limits >> (Toplevel.no_timing oo IsarCmd.pr)); 
7199  873 

7222  874 
val disable_prP = 
875 
OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" K.diag 

9010  876 
(Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr)); 
5832  877 

7222  878 
val enable_prP = 
879 
OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag 

9010  880 
(Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr)); 
7222  881 

5832  882 
val commitP = 
6723  883 
OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag 
9010  884 
(P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.use_commit)); 
5832  885 

886 
val quitP = 

6723  887 
OuterSyntax.improper_command "quit" "quit Isabelle" K.control 
9010  888 
(P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit)); 
5832  889 

890 
val exitP = 

6723  891 
OuterSyntax.improper_command "exit" "exit Isar loop" K.control 
9010  892 
(Scan.succeed (Toplevel.no_timing o IsarCmd.exit)); 
5832  893 

7102  894 
val init_toplevelP = 
895 
OuterSyntax.improper_command "init_toplevel" "restart Isar toplevel loop" K.control 

9010  896 
(Scan.succeed (Toplevel.no_timing o IsarCmd.init_toplevel)); 
5991  897 

7462  898 
val welcomeP = 
8678  899 
OuterSyntax.improper_command "welcome" "print welcome message" K.diag 
9010  900 
(Scan.succeed (Toplevel.no_timing o IsarCmd.welcome)); 
7462  901 

5832  902 

903 

904 
(** the Pure outer syntax **) 

905 

906 
(*keep keywords consistent with the parsers, including those in 

907 
outer_parse.ML, otherwise be prepared for unexpected errors*) 

908 

16038  909 
val _ = OuterSyntax.add_keywords 
17068  910 
["!", "!!", "%", "(", ")", "+", ",", "", ":", "::", ";", "<", "<=", 
21462
74ddf3a522f8
added Isar syntax for adding parameters to axclasses
haftmann
parents:
21437
diff
changeset

911 
"=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes", "attach", 
19809  912 
"begin", "binder", "concl", "constrains", "defines", "fixes", "for", 
913 
"imports", "if", "in", "includes", "infix", "infixl", "infixr", 

914 
"is", "notes", "obtains", "open", "output", "overloaded", "shows", 

19631  915 
"structure", "unchecked", "uses", "where", "", "\\<equiv>", 
18895  916 
"\\<leftharpoondown>", "\\<rightharpoonup>", 
917 
"\\<rightleftharpoons>", "\\<subseteq>"]; 

5832  918 

16038  919 
val _ = OuterSyntax.add_parsers [ 
5832  920 
(*theory structure*) 
21306
7ab6e95e6b0b
turned 'context' into plain thy_decl, discontinued thy_switch;
wenzelm
parents:
21269
diff
changeset

921 
theoryP, endP, 
7775  922 
(*markup commands*) 
7733  923 
headerP, chapterP, sectionP, subsectionP, subsubsectionP, textP, 
7862  924 
text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP, 
5832  925 
(*theory sections*) 
19245  926 
classesP, classrelP, defaultsortP, axclassP, typedeclP, typeabbrP, 
927 
nontermP, aritiesP, judgmentP, constsP, finalconstsP, syntaxP, 

19260  928 
no_syntaxP, translationsP, no_translationsP, axiomsP, defsP, 
21210  929 
constdefsP, definitionP, abbreviationP, notationP, axiomatizationP, 
930 
theoremsP, lemmasP, declareP, globalP, localP, hideP, useP, mlP, 

22088  931 
ml_commandP, ml_setupP, setupP, method_setupP, declarationP, 
19659  932 
parse_ast_translationP, parse_translationP, print_translationP, 
933 
typed_print_translationP, print_ast_translationP, 

21306
7ab6e95e6b0b
turned 'context' into plain thy_decl, discontinued thy_switch;
wenzelm
parents:
21269
diff
changeset

934 
token_translationP, oracleP, contextP, localeP, 
5832  935 
(*proof commands*) 
17353  936 
theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP, 
17854  937 
assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP, 
20958  938 
withP, noteP, usingP, unfoldingP, begin_blockP, end_blockP, nextP, 
939 
qedP, terminal_proofP, default_proofP, immediate_proofP, 

940 
done_proofP, skip_proofP, forget_proofP, deferP, preferP, applyP, 

941 
apply_endP, proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP, 

21956  942 
cannot_undoP, redoP, undos_proofP, undoP, killP, interpretationP, 
943 
interpretP, 

16168
adb83939177f
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16102
diff
changeset

944 
(*diagnostic commands*) 
21714  945 
pretty_setmarginP, helpP, print_commandsP, print_contextP, 
21726  946 
print_theoryP, print_syntaxP, print_abbrevsP, print_factsP, 
947 
print_theoremsP, print_localesP, print_localeP, 

948 
print_registrationsP, print_attributesP, print_simpsetP, 

949 
print_rulesP, print_induct_rulesP, print_trans_rulesP, 

950 
print_methodsP, print_antiquotationsP, class_depsP, thm_depsP, 

951 
find_theoremsP, print_bindsP, print_casesP, print_stmtsP, 

952 
print_thmsP, print_prfsP, print_full_prfsP, print_propP, 

953 
print_termP, print_typeP, 

5832  954 
(*system commands*) 
7102  955 
cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP, 
7931  956 
touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP, 
14934  957 
kill_thyP, display_draftsP, print_draftsP, prP, disable_prP, 
958 
enable_prP, commitP, quitP, exitP, init_toplevelP, welcomeP]; 

5832  959 

960 
end; 