author  wenzelm 
Sat, 21 Jan 2006 23:02:14 +0100  
changeset 18728  6790126ab5f6 
parent 18670  c3f445b92aff 
child 18766  932750b85c5b 
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) 
9129  18 
(ThyHeader.args >> (Toplevel.print oo IsarThy.theory)); 
5832  19 

6687  20 
val end_excursionP = 
17068  21 
OuterSyntax.command "end" "end current excursion" (K.tag_theory K.thy_end) 
6687  22 
(Scan.succeed (Toplevel.print o Toplevel.exit)); 
23 

6245  24 
val contextP = 
17068  25 
OuterSyntax.improper_command "context" "switch theory context" (K.tag_theory K.thy_switch) 
6723  26 
(P.name >> (Toplevel.print oo IsarThy.context)); 
6245  27 

5832  28 

29 

7749  30 
(** markup commands **) 
5832  31 

9129  32 
val headerP = OuterSyntax.markup_command IsarOutput.Markup "header" "theory header" K.diag 
12940  33 
(P.position P.text >> IsarCmd.add_header); 
6353  34 

9129  35 
val chapterP = OuterSyntax.markup_command IsarOutput.Markup "chapter" "chapter heading" 
17264
c5b280a52a67
chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

36 
K.thy_heading (P.opt_locale_target  P.position P.text >> IsarCmd.add_chapter); 
5958  37 

9129  38 
val sectionP = OuterSyntax.markup_command IsarOutput.Markup "section" "section heading" 
17264
c5b280a52a67
chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

39 
K.thy_heading (P.opt_locale_target  P.position P.text >> IsarCmd.add_section); 
5958  40 

9129  41 
val subsectionP = OuterSyntax.markup_command IsarOutput.Markup "subsection" "subsection heading" 
17264
c5b280a52a67
chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

42 
K.thy_heading (P.opt_locale_target  P.position P.text >> IsarCmd.add_subsection); 
5958  43 

7749  44 
val subsubsectionP = 
9129  45 
OuterSyntax.markup_command IsarOutput.Markup "subsubsection" "subsubsection heading" 
17264
c5b280a52a67
chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

46 
K.thy_heading (P.opt_locale_target  P.position P.text >> IsarCmd.add_subsubsection); 
5832  47 

9129  48 
val textP = OuterSyntax.markup_command IsarOutput.MarkupEnv "text" "formal comment (theory)" 
17264
c5b280a52a67
chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

49 
K.thy_decl (P.opt_locale_target  P.position P.text >> IsarCmd.add_text); 
7172  50 

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

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

53 
K.thy_decl (P.position P.text >> IsarCmd.add_text_raw); 
7172  54 

9552  55 
val sectP = OuterSyntax.markup_command IsarOutput.Markup "sect" "formal comment (proof)" 
17068  56 
(K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.add_sect); 
7172  57 

9129  58 
val subsectP = OuterSyntax.markup_command IsarOutput.Markup "subsect" "formal comment (proof)" 
17068  59 
(K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.add_subsect); 
7172  60 

9129  61 
val subsubsectP = OuterSyntax.markup_command IsarOutput.Markup "subsubsect" 
17068  62 
"formal comment (proof)" (K.tag_proof K.prf_heading) 
12940  63 
(P.position P.text >> IsarCmd.add_subsubsect); 
7172  64 

9129  65 
val txtP = OuterSyntax.markup_command IsarOutput.MarkupEnv "txt" "formal comment (proof)" 
17068  66 
(K.tag_proof K.prf_decl) (P.position P.text >> IsarCmd.add_txt); 
7172  67 

9129  68 
val txt_rawP = OuterSyntax.markup_command IsarOutput.Verbatim "txt_raw" 
17068  69 
"raw document preparation text (proof)" (K.tag_proof K.prf_decl) 
12940  70 
(P.position P.text >> IsarCmd.add_txt_raw); 
7775  71 

5832  72 

6886  73 

74 
(** theory sections **) 

75 

5832  76 
(* classes and sorts *) 
77 

78 
val classesP = 

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

80 
(Scan.repeat1 (P.name  Scan.optional ((P.$$$ "\\<subseteq>"  P.$$$ "<")  
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

81 
P.!!! (P.list1 P.xname)) []) >> (Toplevel.theory o Theory.add_classes)); 
5832  82 

83 
val classrelP = 

6723  84 
OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl 
14779  85 
(P.and_list1 (P.xname  ((P.$$$ "\\<subseteq>"  P.$$$ "<")  P.!!! P.xname)) 
86 
>> (Toplevel.theory o Theory.add_classrel)); 

5832  87 

88 
val defaultsortP = 

6723  89 
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

90 
(P.sort >> (Toplevel.theory o Theory.add_defsort)); 
5832  91 

92 

93 
(* types *) 

94 

95 
val typedeclP = 

12624  96 
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

97 
(P.type_args  P.name  P.opt_infix >> (fn ((args, a), mx) => 
16447  98 
Toplevel.theory (Theory.add_typedecls [(a, args, mx)]))); 
5832  99 

100 
val typeabbrP = 

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

103 
(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

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

105 
map (fn ((args, a), (T, mx)) => (a, args, T, mx)))); 
5832  106 

107 
val nontermP = 

6370  108 
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

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

111 
val aritiesP = 

6723  112 
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

113 
(Scan.repeat1 (P.xname  (P.$$$ "::"  P.!!! P.arity) >> P.triple2) 
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

114 
>> (Toplevel.theory o Theory.add_arities)); 
5832  115 

116 

117 
(* consts and syntax *) 

118 

8227  119 
val judgmentP = 
120 
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

121 
(P.const >> (Toplevel.theory o ObjectLogic.add_judgment)); 
8227  122 

5832  123 
val constsP = 
6723  124 
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

125 
(Scan.repeat1 P.const >> (Toplevel.theory o Theory.add_consts)); 
5832  126 

14642  127 
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

128 

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

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

130 
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

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

12142  133 
val mode_spec = 
9731  134 
(P.$$$ "output" >> K ("", false))  P.name  Scan.optional (P.$$$ "output" >> K false) true; 
135 

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

5832  138 

139 
val syntaxP = 

6723  140 
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

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

15748  143 
val no_syntaxP = 
144 
OuterSyntax.command "no_syntax" "delete syntax declarations" K.thy_decl 

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

146 

5832  147 

148 
(* translations *) 

149 

150 
val trans_pat = 

6723  151 
Scan.optional (P.$$$ "("  P.!!! (P.xname  P.$$$ ")")) "logic"  P.string; 
5832  152 

153 
fun trans_arrow toks = 

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

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

5832  157 

158 
val trans_line = 

6723  159 
trans_pat  P.!!! (trans_arrow  trans_pat) 
5832  160 
>> (fn (left, (arr, right)) => arr (left, right)); 
161 

162 
val translationsP = 

6723  163 
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

164 
(Scan.repeat1 trans_line >> (Toplevel.theory o Theory.add_trrules)); 
5832  165 

166 

167 
(* axioms and definitions *) 

168 

169 
val axiomsP = 

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

171 
(Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_axioms)); 
5832  172 

173 
val defsP = 

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

175 
(opt_overloaded  Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_defs)); 
6370  176 

14642  177 

178 
(* constant definitions *) 

179 

180 
val structs = 

18670  181 
Scan.optional ((P.$$$ "("  P.$$$ "structure")  P.!!! (P.simple_fixes  P.$$$ ")")) []; 
14642  182 

183 
val constdecl = 

18670  184 
(P.name  P.$$$ "where") >> (fn x => (x, NONE, NoSyn))  
15531  185 
P.name  (P.$$$ "::"  P.!!! P.typ >> SOME)  P.opt_mixfix' >> P.triple1  
18670  186 
P.name  (P.mixfix >> pair NONE) >> P.triple2; 
14642  187 
val constdef = Scan.option constdecl  (P.opt_thm_name ":"  P.prop); 
188 

6370  189 
val constdefsP = 
14642  190 
OuterSyntax.command "constdefs" "standard constant definitions" K.thy_decl 
191 
(structs  Scan.repeat1 constdef >> (Toplevel.theory o Constdefs.add_constdefs)); 

5832  192 

193 

18616  194 
(* constant specifications *) 
195 

196 
val axiomatizationP = 

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

18670  198 
(P.fixes  Scan.optional (P.$$$ "where"  P.!!! (P.and_list1 P.named_spec)) [] 
18616  199 
>> (Toplevel.theory o (#2 oo Specification.axiomatize))); 
200 

201 

5914  202 
(* theorems *) 
203 

17353  204 
fun theorems kind = P.opt_locale_target  P.name_facts 
205 
>> (Toplevel.theory_context o uncurry (IsarThy.smart_theorems kind)); 

12712  206 

5914  207 
val theoremsP = 
17353  208 
OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems Drule.theoremK); 
5914  209 

210 
val lemmasP = 

17353  211 
OuterSyntax.command "lemmas" "define lemmas" K.thy_decl (theorems Drule.lemmaK); 
5914  212 

9589  213 
val declareP = 
9776  214 
OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script 
16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16604
diff
changeset

215 
(P.opt_locale_target  (P.and_list1 P.xthms1 >> List.concat) 
17107
2c35e00ee2ab
various Toplevel.theory_context commands: proper presentation in context;
wenzelm
parents:
17068
diff
changeset

216 
>> (Toplevel.theory_context o uncurry IsarThy.declare_theorems)); 
9589  217 

5914  218 

5832  219 
(* name space entry path *) 
220 

221 
val globalP = 

6723  222 
OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl 
16447  223 
(Scan.succeed (Toplevel.theory Sign.root_path)); 
5832  224 

225 
val localP = 

6723  226 
OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl 
16447  227 
(Scan.succeed (Toplevel.theory Sign.local_path)); 
8723  228 

229 
val hideP = 

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

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

5832  233 

234 

235 
(* use ML text *) 

236 

237 
val useP = 

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

241 
val mlP = 

17068  242 
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

243 
(P.text >> IsarCmd.use_mltext true); 
7891  244 

245 
val ml_commandP = 

17068  246 
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

247 
(P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false)); 
7616  248 

249 
val ml_setupP = 

17068  250 
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

251 
(P.text >> IsarCmd.use_mltext_theory); 
5832  252 

253 
val setupP = 

17068  254 
OuterSyntax.command "setup" "apply ML theory setup" (K.tag_ml K.thy_decl) 
18670  255 
(Scan.option P.text >> (Toplevel.theory o PureThy.generic_setup)); 
5832  256 

9197  257 
val method_setupP = 
17068  258 
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

259 
(((P.name  P.!!! (P.$$$ "="  P.text  P.text) >> P.triple2)) 
17353  260 
>> (Toplevel.theory o Method.method_setup)); 
9197  261 

5832  262 

263 
(* translation functions *) 

264 

14642  265 
val trfun = P.opt_keyword "advanced"  P.text; 
266 

5832  267 
val parse_ast_translationP = 
17068  268 
OuterSyntax.command "parse_ast_translation" "install parse ast translation functions" 
269 
(K.tag_ml K.thy_decl) 

17107
2c35e00ee2ab
various Toplevel.theory_context commands: proper presentation in context;
wenzelm
parents:
17068
diff
changeset

270 
(trfun >> (Toplevel.theory o Sign.parse_ast_translation)); 
5832  271 

272 
val parse_translationP = 

17068  273 
OuterSyntax.command "parse_translation" "install parse translation functions" 
274 
(K.tag_ml K.thy_decl) 

17107
2c35e00ee2ab
various Toplevel.theory_context commands: proper presentation in context;
wenzelm
parents:
17068
diff
changeset

275 
(trfun >> (Toplevel.theory o Sign.parse_translation)); 
5832  276 

277 
val print_translationP = 

17068  278 
OuterSyntax.command "print_translation" "install print translation functions" 
279 
(K.tag_ml K.thy_decl) 

17107
2c35e00ee2ab
various Toplevel.theory_context commands: proper presentation in context;
wenzelm
parents:
17068
diff
changeset

280 
(trfun >> (Toplevel.theory o Sign.print_translation)); 
5832  281 

282 
val typed_print_translationP = 

6370  283 
OuterSyntax.command "typed_print_translation" "install typed print translation functions" 
17068  284 
(K.tag_ml K.thy_decl) 
17107
2c35e00ee2ab
various Toplevel.theory_context commands: proper presentation in context;
wenzelm
parents:
17068
diff
changeset

285 
(trfun >> (Toplevel.theory o Sign.typed_print_translation)); 
5832  286 

287 
val print_ast_translationP = 

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

17107
2c35e00ee2ab
various Toplevel.theory_context commands: proper presentation in context;
wenzelm
parents:
17068
diff
changeset

290 
(trfun >> (Toplevel.theory o Sign.print_ast_translation)); 
5832  291 

292 
val token_translationP = 

17068  293 
OuterSyntax.command "token_translation" "install token translation functions" 
294 
(K.tag_ml K.thy_decl) 

17107
2c35e00ee2ab
various Toplevel.theory_context commands: proper presentation in context;
wenzelm
parents:
17068
diff
changeset

295 
(P.text >> (Toplevel.theory o Sign.token_translation)); 
5832  296 

297 

298 
(* oracles *) 

299 

300 
val oracleP = 

17068  301 
OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl) 
16849  302 
(P.name  (P.$$$ "("  P.text  P.$$$ ")"  P.$$$ "=") 
17353  303 
 P.text >> (Toplevel.theory o PureThy.add_oracle o P.triple1)); 
5832  304 

305 

12061  306 
(* locales *) 
307 

12758  308 
val locale_val = 
309 
(P.locale_expr  

18136  310 
Scan.optional (P.$$$ "+"  P.!!! (Scan.repeat1 P.context_element)) []  
311 
Scan.repeat1 P.context_element >> pair Locale.empty); 

12061  312 

313 
val localeP = 

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

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

18670  317 
>> (Toplevel.theory_context o (fn ((x, y), (z, w)) => 
318 
Locale.add_locale_context x y z w #> (fn ((_, ctxt), thy) => (thy, ctxt))))); 

12061  319 

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

320 
val opt_inst = 
17353  321 
Scan.optional (P.$$$ "["  P.!!! (Scan.repeat1 (P.maybe P.term)  P.$$$ "]")) []; 
15596  322 

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

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

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

325 
"prove and register interpretation of locale expression in theory or locale" K.thy_goal 
17353  326 
(P.xname  (P.$$$ "\\<subseteq>"  P.$$$ "<")  P.!!! P.locale_expr 
327 
>> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale))  

328 
P.opt_thm_name ":"  P.locale_expr  opt_inst >> (fn ((x, y), z) => 

329 
Toplevel.print o Toplevel.theory_to_proof (Locale.interpretation x y z))); 

12061  330 

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

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

332 
OuterSyntax.command "interpret" 
17068  333 
"prove and register interpretation of locale expression in proof context" 
334 
(K.tag_proof K.prf_goal) 

17353  335 
(P.opt_thm_name ":"  P.locale_expr  opt_inst >> (fn ((x, y), z) => 
17900  336 
Toplevel.print o Toplevel.proof' (Locale.interpret x y z))); 
15703  337 

338 

5832  339 

340 
(** proof commands **) 

341 

342 
(* statements *) 

343 

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

344 
val statement = P.and_list1 (P.opt_thm_name ":"  Scan.repeat1 P.propp); 
12956  345 
val general_statement = 
18136  346 
statement >> pair []  Scan.repeat P.locale_element  (P.$$$ "shows"  statement); 
5832  347 

17353  348 
fun gen_theorem kind = 
349 
OuterSyntax.command kind ("state " ^ kind) K.thy_goal 

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

350 
(P.opt_locale_target  Scan.optional (P.opt_thm_name ":"  
12956  351 
Scan.ahead (P.locale_keyword  P.$$$ "shows")) ("", [])  
352 
general_statement >> (fn ((x, y), (z, w)) => 

17353  353 
(Toplevel.print o Toplevel.theory_to_proof (Locale.smart_theorem kind x y z w)))); 
5832  354 

12242
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12142
diff
changeset

355 
val theoremP = gen_theorem Drule.theoremK; 
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12142
diff
changeset

356 
val lemmaP = gen_theorem Drule.lemmaK; 
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12142
diff
changeset

357 
val corollaryP = gen_theorem Drule.corollaryK; 
5832  358 

17353  359 
val haveP = 
360 
OuterSyntax.command "have" "state local goal" 

361 
(K.tag_proof K.prf_goal) 

17900  362 
(statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.have)); 
17353  363 

364 
val henceP = 

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

366 
(K.tag_proof K.prf_goal) 

17900  367 
(statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.hence)); 
17353  368 

5832  369 
val showP = 
17068  370 
OuterSyntax.command "show" "state local goal, solving current obligation" 
371 
(K.tag_proof K.prf_goal) 

17900  372 
(statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.show)); 
5832  373 

6501  374 
val thusP = 
17068  375 
OuterSyntax.command "thus" "abbreviates \"then show\"" 
376 
(K.tag_proof K.prf_goal) 

17900  377 
(statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.thus)); 
6501  378 

5832  379 

5914  380 
(* facts *) 
5832  381 

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

382 
val facts = P.and_list1 P.xthms1; 
9197  383 

5832  384 
val thenP = 
17068  385 
OuterSyntax.command "then" "forward chaining" 
386 
(K.tag_proof K.prf_chain) 

17900  387 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain)); 
5832  388 

389 
val fromP = 

17068  390 
OuterSyntax.command "from" "forward chaining from given facts" 
391 
(K.tag_proof K.prf_chain) 

17900  392 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss))); 
5914  393 

6878  394 
val withP = 
17068  395 
OuterSyntax.command "with" "forward chaining from given and current facts" 
396 
(K.tag_proof K.prf_chain) 

17900  397 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss))); 
6878  398 

6773  399 
val noteP = 
17068  400 
OuterSyntax.command "note" "define facts" 
401 
(K.tag_proof K.prf_decl) 

17900  402 
(P.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss))); 
5832  403 

12926  404 
val usingP = 
17068  405 
OuterSyntax.command "using" "augment goal facts" 
406 
(K.tag_proof K.prf_decl) 

18544  407 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.using))); 
408 

409 
val unfoldingP = 

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

411 
(K.tag_proof K.prf_decl) 

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

12926  413 

5832  414 

415 
(* proof context *) 

416 

11890  417 
val fixP = 
17068  418 
OuterSyntax.command "fix" "fix local variables (Skolem constants)" 
419 
(K.tag_proof K.prf_asm) 

18670  420 
(P.simple_fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix))); 
11890  421 

5832  422 
val assumeP = 
17068  423 
OuterSyntax.command "assume" "assume propositions" 
424 
(K.tag_proof K.prf_asm) 

17900  425 
(statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume))); 
5832  426 

6850  427 
val presumeP = 
17068  428 
OuterSyntax.command "presume" "assume propositions, to be established later" 
429 
(K.tag_proof K.prf_asm) 

17900  430 
(statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume))); 
6850  431 

6953  432 
val defP = 
17068  433 
OuterSyntax.command "def" "local definition" 
434 
(K.tag_proof K.prf_asm) 

18308  435 
(P.and_list1 
436 
(P.opt_thm_name ":"  (P.name  ((P.$$$ "\\<equiv>"  P.$$$ "==")  P.!!! P.termp))) 

437 
>> (Toplevel.print oo (Toplevel.proof o Proof.def))); 

6953  438 

11890  439 
val obtainP = 
440 
OuterSyntax.command "obtain" "generalized existence" 

17068  441 
(K.tag_proof K.prf_asm_goal) 
18670  442 
(Scan.optional (P.simple_fixes  P.$$$ "where") []  statement 
17900  443 
>> (Toplevel.print oo (Toplevel.proof' o uncurry Obtain.obtain))); 
5832  444 

17854  445 
val guessP = 
446 
OuterSyntax.command "guess" "wild guessing (unstructured)" 

447 
(K.tag_proof K.prf_asm_goal) 

18670  448 
(Scan.optional P.simple_fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess))); 
17854  449 

5832  450 
val letP = 
17068  451 
OuterSyntax.command "let" "bind text variables" 
452 
(K.tag_proof K.prf_decl) 

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

453 
(P.and_list1 (P.enum1 "and" P.term  (P.$$$ "="  P.term)) 
17900  454 
>> (Toplevel.print oo (Toplevel.proof o Proof.let_bind))); 
5832  455 

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

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

459 

8370  460 
val caseP = 
17068  461 
OuterSyntax.command "case" "invoke local context" 
462 
(K.tag_proof K.prf_asm) 

17900  463 
(case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case))); 
8370  464 

5832  465 

466 
(* proof structure *) 

467 

468 
val beginP = 

17068  469 
OuterSyntax.command "{" "begin explicit proof block" 
470 
(K.tag_proof K.prf_open) 

17900  471 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block)); 
5832  472 

6687  473 
val endP = 
17068  474 
OuterSyntax.command "}" "end explicit proof block" 
475 
(K.tag_proof K.prf_close) 

17900  476 
(Scan.succeed (Toplevel.print o Toplevel.proofs Proof.end_block)); 
6687  477 

5832  478 
val nextP = 
17068  479 
OuterSyntax.command "next" "enter next proof block" 
480 
(K.tag_proof K.prf_block) 

17900  481 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block)); 
5832  482 

483 

484 
(* end proof *) 

485 

6404  486 
val qedP = 
17068  487 
OuterSyntax.command "qed" "conclude (sub)proof" 
488 
(K.tag_proof K.qed_block) 

17353  489 
(Scan.option P.method >> (Toplevel.print3 oo IsarThy.qed)); 
5832  490 

6404  491 
val terminal_proofP = 
17068  492 
OuterSyntax.command "by" "terminal backward proof" 
493 
(K.tag_proof K.qed) 

17353  494 
(P.method  Scan.option P.method >> (Toplevel.print3 oo IsarThy.terminal_proof)); 
6404  495 

8966  496 
val default_proofP = 
17068  497 
OuterSyntax.command ".." "default proof" 
498 
(K.tag_proof K.qed) 

17353  499 
(Scan.succeed (Toplevel.print3 o IsarThy.default_proof)); 
8966  500 

6404  501 
val immediate_proofP = 
17068  502 
OuterSyntax.command "." "immediate proof" 
503 
(K.tag_proof K.qed) 

17353  504 
(Scan.succeed (Toplevel.print3 o IsarThy.immediate_proof)); 
6404  505 

8966  506 
val done_proofP = 
17068  507 
OuterSyntax.command "done" "done proof" 
508 
(K.tag_proof K.qed) 

17353  509 
(Scan.succeed (Toplevel.print3 o IsarThy.done_proof)); 
5832  510 

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

511 
val skip_proofP = 
17068  512 
OuterSyntax.improper_command "sorry" "skip proof (quickanddirty mode only!)" 
513 
(K.tag_proof K.qed) 

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

515 

8210  516 
val forget_proofP = 
17068  517 
OuterSyntax.command "oops" "forget proof" 
518 
(K.tag_proof K.qed_global) 

18561  519 
(Scan.succeed Toplevel.forget_proof); 
8210  520 

5832  521 

522 
(* proof steps *) 

523 

8165  524 
val deferP = 
17068  525 
OuterSyntax.command "defer" "shuffle internal proof state" 
526 
(K.tag_proof K.prf_script) 

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

529 
val preferP = 

17068  530 
OuterSyntax.command "prefer" "shuffle internal proof state" 
531 
(K.tag_proof K.prf_script) 

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

6850  534 
val applyP = 
17068  535 
OuterSyntax.command "apply" "initial refinement step (unstructured)" 
536 
(K.tag_proof K.prf_script) 

17900  537 
(P.method >> (Toplevel.print oo (Toplevel.proofs o Proof.apply))); 
5832  538 

8235  539 
val apply_endP = 
17068  540 
OuterSyntax.command "apply_end" "terminal refinement (unstructured)" 
541 
(K.tag_proof K.prf_script) 

17900  542 
(P.method >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end))); 
5832  543 

6404  544 
val proofP = 
17068  545 
OuterSyntax.command "proof" "backward proof" 
546 
(K.tag_proof K.prf_block) 

16812  547 
(Scan.option P.method >> (fn m => Toplevel.print o 
17107
2c35e00ee2ab
various Toplevel.theory_context commands: proper presentation in context;
wenzelm
parents:
17068
diff
changeset

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

549 
Toplevel.skip_proof (History.apply (fn i => i + 1)))); 
5832  550 

551 

6773  552 
(* calculational proof commands *) 
553 

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

555 
Scan.option (P.$$$ "("  P.!!! ((P.xthms1  P.$$$ ")"))); 
6878  556 

6773  557 
val alsoP = 
17068  558 
OuterSyntax.command "also" "combine calculation and current facts" 
559 
(K.tag_proof K.prf_decl) 

17900  560 
(calc_args >> (Toplevel.proofs' o Calculation.also)); 
6773  561 

562 
val finallyP = 

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

17900  565 
(calc_args >> (Toplevel.proofs' o Calculation.finally)); 
6773  566 

8562  567 
val moreoverP = 
17068  568 
OuterSyntax.command "moreover" "augment calculation by current facts" 
569 
(K.tag_proof K.prf_decl) 

17900  570 
(Scan.succeed (Toplevel.proof' Calculation.moreover)); 
8562  571 

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

17068  574 
(K.tag_proof K.prf_chain) 
17900  575 
(Scan.succeed (Toplevel.proof' Calculation.ultimately)); 
8588  576 

6773  577 

6742  578 
(* proof navigation *) 
5944  579 

5832  580 
val backP = 
17068  581 
OuterSyntax.command "back" "backtracking of proof command" 
582 
(K.tag_proof K.prf_script) 

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

5832  584 

585 

6742  586 
(* history *) 
587 

588 
val cannot_undoP = 

589 
OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control 

9010  590 
(P.name >> (Toplevel.no_timing oo IsarCmd.cannot_undo)); 
6742  591 

7733  592 
val clear_undosP = 
593 
OuterSyntax.improper_command "clear_undos" "clear theorylevel undo information" K.control 

9010  594 
(P.nat >> (Toplevel.no_timing oo IsarCmd.clear_undos_theory)); 
6742  595 

596 
val redoP = 

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

9010  598 
(Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.redo)); 
6742  599 

600 
val undos_proofP = 

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

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

604 
val undoP = 

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

9010  606 
(Scan.succeed ((Toplevel.no_timing o Toplevel.print) o IsarCmd.undo)); 
6742  607 

8500  608 
val killP = 
609 
OuterSyntax.improper_command "kill" "kill current history node" K.control 

9010  610 
(Scan.succeed ((Toplevel.no_timing o Toplevel.print) o IsarCmd.kill)); 
8500  611 

6742  612 

5832  613 

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

615 

8464  616 
val opt_modes = Scan.optional (P.$$$ "("  P.!!! (Scan.repeat1 P.xname  P.$$$ ")")) []; 
617 

618 

7124  619 
val pretty_setmarginP = 
620 
OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing" 

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

5832  623 
val print_commandsP = 
9221  624 
OuterSyntax.improper_command "print_commands" "print outer syntax (global)" K.diag 
625 
(Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands)); 

5832  626 

7308  627 
val print_contextP = 
628 
OuterSyntax.improper_command "print_context" "print theory context name" K.diag 

9010  629 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_context)); 
7308  630 

5832  631 
val print_theoryP = 
6723  632 
OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag 
9010  633 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_theory)); 
5832  634 

635 
val print_syntaxP = 

6723  636 
OuterSyntax.improper_command "print_syntax" "print inner syntax of theory (verbose!)" K.diag 
9010  637 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax)); 
5832  638 

5881  639 
val print_theoremsP = 
17068  640 
OuterSyntax.improper_command "print_theorems" 
641 
"print theorems of local theory or proof context" K.diag 

9010  642 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_theorems)); 
5881  643 

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

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

647 

648 
val print_localeP = 

15596  649 
OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag 
18670  650 
(Scan.optional (P.$$$ "!" >> K true) false  locale_val 
651 
>> (Toplevel.no_timing oo IsarCmd.print_locale)); 

12061  652 

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

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

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

15596  658 

5832  659 
val print_attributesP = 
12061  660 
OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag 
9010  661 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes)); 
5832  662 

16027  663 
val print_simpsetP = 
664 
OuterSyntax.improper_command "print_simpset" "print context of Simplifier" K.diag 

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

666 

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

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

670 

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

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

674 

9221  675 
val print_trans_rulesP = 
11666  676 
OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" K.diag 
9221  677 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules)); 
678 

5832  679 
val print_methodsP = 
12061  680 
OuterSyntax.improper_command "print_methods" "print methods of this theory" K.diag 
9010  681 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods)); 
5832  682 

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

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

686 

9454  687 
val thm_depsP = 
688 
OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies" 

689 
K.diag (P.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps)); 

690 

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

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

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

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

16074  696 
P.reserved "simp"  P.!!! (P.$$$ ":"  P.term) >> FindTheorems.Simp  
16027  697 
P.term >> FindTheorems.Pattern; 
698 

699 
val find_theoremsP = 

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

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

701 
"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

702 
(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

703 
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

704 
>> (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

705 

5832  706 
val print_bindsP = 
6723  707 
OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag 
9010  708 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds)); 
5832  709 

710 
val print_lthmsP = 

8370  711 
OuterSyntax.improper_command "print_facts" "print facts of proof context" K.diag 
9010  712 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_lthms)); 
5832  713 

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

9010  716 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases)); 
8370  717 

5896  718 
val print_thmsP = 
8464  719 
OuterSyntax.improper_command "thm" "print theorems" K.diag 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

720 
(opt_modes  P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms)); 
5832  721 

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

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

723 
OuterSyntax.improper_command "prf" "print proof terms of theorems" K.diag 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

724 
(opt_modes  Scan.option P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs false)); 
11524
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11101
diff
changeset

725 

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

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

727 
OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" K.diag 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

728 
(opt_modes  Scan.option P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true)); 
11524
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11101
diff
changeset

729 

5832  730 
val print_propP = 
6723  731 
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

732 
(opt_modes  P.term >> (Toplevel.no_timing oo IsarCmd.print_prop)); 
5832  733 

734 
val print_termP = 

6723  735 
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

736 
(opt_modes  P.term >> (Toplevel.no_timing oo IsarCmd.print_term)); 
5832  737 

738 
val print_typeP = 

6723  739 
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

740 
(opt_modes  P.typ >> (Toplevel.no_timing oo IsarCmd.print_type)); 
5832  741 

742 

743 

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

745 

746 
val cdP = 

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

750 
val pwdP = 

6723  751 
OuterSyntax.improper_command "pwd" "print current working directory" K.diag 
9010  752 
(Scan.succeed (Toplevel.no_timing o IsarCmd.pwd)); 
5832  753 

754 
val use_thyP = 

6723  755 
OuterSyntax.improper_command "use_thy" "use theory file" K.diag 
9010  756 
(P.name >> (Toplevel.no_timing oo IsarCmd.use_thy)); 
5832  757 

6694  758 
val use_thy_onlyP = 
7102  759 
OuterSyntax.improper_command "use_thy_only" "use theory file only, ignoring associated ML" 
9010  760 
K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy_only)); 
6694  761 

6196  762 
val update_thyP = 
6723  763 
OuterSyntax.improper_command "update_thy" "update theory file" K.diag 
9010  764 
(P.name >> (Toplevel.no_timing oo IsarCmd.update_thy)); 
5832  765 

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

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

770 
val touch_thyP = 

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

9010  772 
(P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy)); 
7102  773 

774 
val touch_all_thysP = 

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

9010  776 
(Scan.succeed (Toplevel.no_timing o IsarCmd.touch_all_thys)); 
7102  777 

7908  778 
val touch_child_thysP = 
779 
OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag 

9010  780 
(P.name >> (Toplevel.no_timing oo IsarCmd.touch_child_thys)); 
7908  781 

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

9010  784 
(P.name >> (Toplevel.no_timing oo IsarCmd.remove_thy)); 
7102  785 

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

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

14934  790 
val display_draftsP = 
791 
OuterSyntax.improper_command "display_drafts" "display raw source files with symbols" 

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

794 
val print_draftsP = 

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

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

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

800 

5832  801 
val prP = 
8886  802 
OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag 
9731  803 
(opt_modes  opt_limits >> (Toplevel.no_timing oo IsarCmd.pr)); 
7199  804 

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

9010  807 
(Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr)); 
5832  808 

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

9010  811 
(Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr)); 
7222  812 

5832  813 
val commitP = 
6723  814 
OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag 
9010  815 
(P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.use_commit)); 
5832  816 

817 
val quitP = 

6723  818 
OuterSyntax.improper_command "quit" "quit Isabelle" K.control 
9010  819 
(P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit)); 
5832  820 

821 
val exitP = 

6723  822 
OuterSyntax.improper_command "exit" "exit Isar loop" K.control 
9010  823 
(Scan.succeed (Toplevel.no_timing o IsarCmd.exit)); 
5832  824 

7102  825 
val init_toplevelP = 
826 
OuterSyntax.improper_command "init_toplevel" "restart Isar toplevel loop" K.control 

9010  827 
(Scan.succeed (Toplevel.no_timing o IsarCmd.init_toplevel)); 
5991  828 

7462  829 
val welcomeP = 
8678  830 
OuterSyntax.improper_command "welcome" "print welcome message" K.diag 
9010  831 
(Scan.succeed (Toplevel.no_timing o IsarCmd.welcome)); 
7462  832 

5832  833 

834 

835 
(** the Pure outer syntax **) 

836 

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

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

839 

16038  840 
val _ = OuterSyntax.add_keywords 
17068  841 
["!", "!!", "%", "(", ")", "+", ",", "", ":", "::", ";", "<", "<=", 
842 
"=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes", 

16264  843 
"begin", "binder", "concl", "constrains", "defines", "files", 
844 
"fixes", "imports", "in", "includes", "infix", "infixl", "infixr", 

845 
"is", "notes", "open", "output", "overloaded", "shows", "structure", 

846 
"uses", "where", "", "\\<equiv>", "\\<leftharpoondown>", 

847 
"\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>"]; 

5832  848 

16038  849 
val _ = OuterSyntax.add_parsers [ 
5832  850 
(*theory structure*) 
8500  851 
theoryP, end_excursionP, contextP, 
7775  852 
(*markup commands*) 
7733  853 
headerP, chapterP, sectionP, subsectionP, subsubsectionP, textP, 
7862  854 
text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP, 
5832  855 
(*theory sections*) 
7172  856 
classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP, 
15748  857 
aritiesP, judgmentP, constsP, finalconstsP, syntaxP, no_syntaxP, 
18616  858 
translationsP, axiomsP, defsP, constdefsP, axiomatizationP, 
859 
theoremsP, lemmasP, declareP, globalP, localP, hideP, useP, mlP, 

860 
ml_commandP, ml_setupP, setupP, method_setupP, 

861 
parse_ast_translationP, parse_translationP, print_translationP, 

862 
typed_print_translationP, print_ast_translationP, 

863 
token_translationP, oracleP, localeP, 

5832  864 
(*proof commands*) 
17353  865 
theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP, 
17854  866 
assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP, 
18544  867 
withP, noteP, usingP, unfoldingP, beginP, endP, nextP, qedP, 
868 
terminal_proofP, default_proofP, immediate_proofP, done_proofP, 

869 
skip_proofP, forget_proofP, deferP, preferP, applyP, apply_endP, 

870 
proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP, 

871 
cannot_undoP, clear_undosP, redoP, undos_proofP, undoP, killP, 

872 
interpretationP, interpretP, 

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

873 
(*diagnostic commands*) 
adb83939177f
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16102
diff
changeset

874 
pretty_setmarginP, 
16027  875 
print_commandsP, print_contextP, print_theoryP, print_syntaxP, 
876 
print_theoremsP, print_localesP, print_localeP, 

877 
print_registrationsP, print_attributesP, print_simpsetP, 

878 
print_rulesP, print_induct_rulesP, print_trans_rulesP, 

879 
print_methodsP, print_antiquotationsP, thm_depsP, find_theoremsP, 

880 
print_bindsP, print_lthmsP, print_casesP, print_thmsP, print_prfsP, 

881 
print_full_prfsP, print_propP, print_termP, print_typeP, 

5832  882 
(*system commands*) 
7102  883 
cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP, 
7931  884 
touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP, 
14934  885 
kill_thyP, display_draftsP, print_draftsP, prP, disable_prP, 
886 
enable_prP, commitP, quitP, exitP, init_toplevelP, welcomeP]; 

5832  887 

888 
end; 