author  wenzelm 
Sat, 28 Jan 2006 17:28:56 +0100  
changeset 18822  9dc194c479aa 
parent 18799  f137c5e971f5 
child 18895  324bcc35570d 
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 = 
18780  190 
OuterSyntax.command "constdefs" "oldstyle constant definitions" K.thy_decl 
14642  191 
(structs  Scan.repeat1 constdef >> (Toplevel.theory o Constdefs.add_constdefs)); 
5832  192 

18780  193 
val definitionP = 
194 
OuterSyntax.command "definition" "standard constant definition" K.thy_decl 

195 
(P.opt_locale_target  Scan.repeat1 constdef 

196 
>> (fn (x, y) => Toplevel.theory_context (#2 o Specification.definition x y))); 

197 

5832  198 

18616  199 
(* constant specifications *) 
200 

201 
val axiomatizationP = 

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

18766  203 
(P.opt_locale_target  
204 
Scan.optional P.fixes []  

18780  205 
Scan.optional (P.$$$ "where"  P.!!! (P.and_list1 P.spec)) [] 
18766  206 
>> (fn ((x, y), z) => Toplevel.theory_context (#2 o Specification.axiomatization x y z))); 
18616  207 

208 

5914  209 
(* theorems *) 
210 

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

12712  213 

5914  214 
val theoremsP = 
18799  215 
OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems PureThy.theoremK); 
5914  216 

217 
val lemmasP = 

18799  218 
OuterSyntax.command "lemmas" "define lemmas" K.thy_decl (theorems PureThy.lemmaK); 
5914  219 

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

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

223 
>> (Toplevel.theory_context o uncurry IsarThy.declare_theorems)); 
9589  224 

5914  225 

5832  226 
(* name space entry path *) 
227 

228 
val globalP = 

6723  229 
OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl 
16447  230 
(Scan.succeed (Toplevel.theory Sign.root_path)); 
5832  231 

232 
val localP = 

6723  233 
OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl 
16447  234 
(Scan.succeed (Toplevel.theory Sign.local_path)); 
8723  235 

236 
val hideP = 

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

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

5832  240 

241 

242 
(* use ML text *) 

243 

244 
val useP = 

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

248 
val mlP = 

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

250 
(P.text >> IsarCmd.use_mltext true); 
7891  251 

252 
val ml_commandP = 

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

254 
(P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false)); 
7616  255 

256 
val ml_setupP = 

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

258 
(P.text >> IsarCmd.use_mltext_theory); 
5832  259 

260 
val setupP = 

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

9197  264 
val method_setupP = 
17068  265 
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

266 
(((P.name  P.!!! (P.$$$ "="  P.text  P.text) >> P.triple2)) 
17353  267 
>> (Toplevel.theory o Method.method_setup)); 
9197  268 

5832  269 

270 
(* translation functions *) 

271 

14642  272 
val trfun = P.opt_keyword "advanced"  P.text; 
273 

5832  274 
val parse_ast_translationP = 
17068  275 
OuterSyntax.command "parse_ast_translation" "install parse ast translation functions" 
276 
(K.tag_ml K.thy_decl) 

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

277 
(trfun >> (Toplevel.theory o Sign.parse_ast_translation)); 
5832  278 

279 
val parse_translationP = 

17068  280 
OuterSyntax.command "parse_translation" "install parse translation functions" 
281 
(K.tag_ml K.thy_decl) 

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

282 
(trfun >> (Toplevel.theory o Sign.parse_translation)); 
5832  283 

284 
val print_translationP = 

17068  285 
OuterSyntax.command "print_translation" "install print translation functions" 
286 
(K.tag_ml K.thy_decl) 

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

287 
(trfun >> (Toplevel.theory o Sign.print_translation)); 
5832  288 

289 
val typed_print_translationP = 

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

292 
(trfun >> (Toplevel.theory o Sign.typed_print_translation)); 
5832  293 

294 
val print_ast_translationP = 

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

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

297 
(trfun >> (Toplevel.theory o Sign.print_ast_translation)); 
5832  298 

299 
val token_translationP = 

17068  300 
OuterSyntax.command "token_translation" "install token translation functions" 
301 
(K.tag_ml K.thy_decl) 

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

302 
(P.text >> (Toplevel.theory o Sign.token_translation)); 
5832  303 

304 

305 
(* oracles *) 

306 

307 
val oracleP = 

17068  308 
OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl) 
16849  309 
(P.name  (P.$$$ "("  P.text  P.$$$ ")"  P.$$$ "=") 
17353  310 
 P.text >> (Toplevel.theory o PureThy.add_oracle o P.triple1)); 
5832  311 

312 

12061  313 
(* locales *) 
314 

12758  315 
val locale_val = 
316 
(P.locale_expr  

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

12061  319 

320 
val localeP = 

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

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

18670  324 
>> (Toplevel.theory_context o (fn ((x, y), (z, w)) => 
18799  325 
Locale.add_locale_context x y z w #> (fn ((_, ctxt), thy) => (ctxt, thy))))); 
12061  326 

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

327 
val opt_inst = 
17353  328 
Scan.optional (P.$$$ "["  P.!!! (Scan.repeat1 (P.maybe P.term)  P.$$$ "]")) []; 
15596  329 

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

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

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

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

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

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

12061  337 

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

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

339 
OuterSyntax.command "interpret" 
17068  340 
"prove and register interpretation of locale expression in proof context" 
341 
(K.tag_proof K.prf_goal) 

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

345 

5832  346 

347 
(** proof commands **) 

348 

349 
(* statements *) 

350 

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

351 
val statement = P.and_list1 (P.opt_thm_name ":"  Scan.repeat1 P.propp); 
12956  352 
val general_statement = 
18136  353 
statement >> pair []  Scan.repeat P.locale_element  (P.$$$ "shows"  statement); 
5832  354 

17353  355 
fun gen_theorem kind = 
356 
OuterSyntax.command kind ("state " ^ kind) K.thy_goal 

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

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

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

18799  362 
val theoremP = gen_theorem PureThy.theoremK; 
363 
val lemmaP = gen_theorem PureThy.lemmaK; 

364 
val corollaryP = gen_theorem PureThy.corollaryK; 

5832  365 

17353  366 
val haveP = 
367 
OuterSyntax.command "have" "state local goal" 

368 
(K.tag_proof K.prf_goal) 

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

371 
val henceP = 

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

373 
(K.tag_proof K.prf_goal) 

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

5832  376 
val showP = 
17068  377 
OuterSyntax.command "show" "state local goal, solving current obligation" 
378 
(K.tag_proof K.prf_goal) 

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

6501  381 
val thusP = 
17068  382 
OuterSyntax.command "thus" "abbreviates \"then show\"" 
383 
(K.tag_proof K.prf_goal) 

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

5832  386 

5914  387 
(* facts *) 
5832  388 

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

389 
val facts = P.and_list1 P.xthms1; 
9197  390 

5832  391 
val thenP = 
17068  392 
OuterSyntax.command "then" "forward chaining" 
393 
(K.tag_proof K.prf_chain) 

17900  394 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain)); 
5832  395 

396 
val fromP = 

17068  397 
OuterSyntax.command "from" "forward chaining from given facts" 
398 
(K.tag_proof K.prf_chain) 

17900  399 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss))); 
5914  400 

6878  401 
val withP = 
17068  402 
OuterSyntax.command "with" "forward chaining from given and current facts" 
403 
(K.tag_proof K.prf_chain) 

17900  404 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss))); 
6878  405 

6773  406 
val noteP = 
17068  407 
OuterSyntax.command "note" "define facts" 
408 
(K.tag_proof K.prf_decl) 

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

12926  411 
val usingP = 
17068  412 
OuterSyntax.command "using" "augment goal facts" 
413 
(K.tag_proof K.prf_decl) 

18544  414 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.using))); 
415 

416 
val unfoldingP = 

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

418 
(K.tag_proof K.prf_decl) 

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

12926  420 

5832  421 

422 
(* proof context *) 

423 

11890  424 
val fixP = 
17068  425 
OuterSyntax.command "fix" "fix local variables (Skolem constants)" 
426 
(K.tag_proof K.prf_asm) 

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

5832  429 
val assumeP = 
17068  430 
OuterSyntax.command "assume" "assume propositions" 
431 
(K.tag_proof K.prf_asm) 

17900  432 
(statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume))); 
5832  433 

6850  434 
val presumeP = 
17068  435 
OuterSyntax.command "presume" "assume propositions, to be established later" 
436 
(K.tag_proof K.prf_asm) 

17900  437 
(statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume))); 
6850  438 

6953  439 
val defP = 
17068  440 
OuterSyntax.command "def" "local definition" 
441 
(K.tag_proof K.prf_asm) 

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

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

6953  445 

11890  446 
val obtainP = 
447 
OuterSyntax.command "obtain" "generalized existence" 

17068  448 
(K.tag_proof K.prf_asm_goal) 
18670  449 
(Scan.optional (P.simple_fixes  P.$$$ "where") []  statement 
17900  450 
>> (Toplevel.print oo (Toplevel.proof' o uncurry Obtain.obtain))); 
5832  451 

17854  452 
val guessP = 
453 
OuterSyntax.command "guess" "wild guessing (unstructured)" 

454 
(K.tag_proof K.prf_asm_goal) 

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

5832  457 
val letP = 
17068  458 
OuterSyntax.command "let" "bind text variables" 
459 
(K.tag_proof K.prf_decl) 

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

460 
(P.and_list1 (P.enum1 "and" P.term  (P.$$$ "="  P.term)) 
17900  461 
>> (Toplevel.print oo (Toplevel.proof o Proof.let_bind))); 
5832  462 

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

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

466 

8370  467 
val caseP = 
17068  468 
OuterSyntax.command "case" "invoke local context" 
469 
(K.tag_proof K.prf_asm) 

17900  470 
(case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case))); 
8370  471 

5832  472 

473 
(* proof structure *) 

474 

475 
val beginP = 

17068  476 
OuterSyntax.command "{" "begin explicit proof block" 
477 
(K.tag_proof K.prf_open) 

17900  478 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block)); 
5832  479 

6687  480 
val endP = 
17068  481 
OuterSyntax.command "}" "end explicit proof block" 
482 
(K.tag_proof K.prf_close) 

17900  483 
(Scan.succeed (Toplevel.print o Toplevel.proofs Proof.end_block)); 
6687  484 

5832  485 
val nextP = 
17068  486 
OuterSyntax.command "next" "enter next proof block" 
487 
(K.tag_proof K.prf_block) 

17900  488 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block)); 
5832  489 

490 

491 
(* end proof *) 

492 

6404  493 
val qedP = 
17068  494 
OuterSyntax.command "qed" "conclude (sub)proof" 
495 
(K.tag_proof K.qed_block) 

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

6404  498 
val terminal_proofP = 
17068  499 
OuterSyntax.command "by" "terminal backward proof" 
500 
(K.tag_proof K.qed) 

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

8966  503 
val default_proofP = 
17068  504 
OuterSyntax.command ".." "default proof" 
505 
(K.tag_proof K.qed) 

17353  506 
(Scan.succeed (Toplevel.print3 o IsarThy.default_proof)); 
8966  507 

6404  508 
val immediate_proofP = 
17068  509 
OuterSyntax.command "." "immediate proof" 
510 
(K.tag_proof K.qed) 

17353  511 
(Scan.succeed (Toplevel.print3 o IsarThy.immediate_proof)); 
6404  512 

8966  513 
val done_proofP = 
17068  514 
OuterSyntax.command "done" "done proof" 
515 
(K.tag_proof K.qed) 

17353  516 
(Scan.succeed (Toplevel.print3 o IsarThy.done_proof)); 
5832  517 

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

518 
val skip_proofP = 
17068  519 
OuterSyntax.improper_command "sorry" "skip proof (quickanddirty mode only!)" 
520 
(K.tag_proof K.qed) 

17353  521 
(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

522 

8210  523 
val forget_proofP = 
17068  524 
OuterSyntax.command "oops" "forget proof" 
525 
(K.tag_proof K.qed_global) 

18561  526 
(Scan.succeed Toplevel.forget_proof); 
8210  527 

5832  528 

529 
(* proof steps *) 

530 

8165  531 
val deferP = 
17068  532 
OuterSyntax.command "defer" "shuffle internal proof state" 
533 
(K.tag_proof K.prf_script) 

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

536 
val preferP = 

17068  537 
OuterSyntax.command "prefer" "shuffle internal proof state" 
538 
(K.tag_proof K.prf_script) 

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

6850  541 
val applyP = 
17068  542 
OuterSyntax.command "apply" "initial refinement step (unstructured)" 
543 
(K.tag_proof K.prf_script) 

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

8235  546 
val apply_endP = 
17068  547 
OuterSyntax.command "apply_end" "terminal refinement (unstructured)" 
548 
(K.tag_proof K.prf_script) 

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

6404  551 
val proofP = 
17068  552 
OuterSyntax.command "proof" "backward proof" 
553 
(K.tag_proof K.prf_block) 

16812  554 
(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

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

556 
Toplevel.skip_proof (History.apply (fn i => i + 1)))); 
5832  557 

558 

6773  559 
(* calculational proof commands *) 
560 

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

562 
Scan.option (P.$$$ "("  P.!!! ((P.xthms1  P.$$$ ")"))); 
6878  563 

6773  564 
val alsoP = 
17068  565 
OuterSyntax.command "also" "combine calculation and current facts" 
566 
(K.tag_proof K.prf_decl) 

17900  567 
(calc_args >> (Toplevel.proofs' o Calculation.also)); 
6773  568 

569 
val finallyP = 

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

17900  572 
(calc_args >> (Toplevel.proofs' o Calculation.finally)); 
6773  573 

8562  574 
val moreoverP = 
17068  575 
OuterSyntax.command "moreover" "augment calculation by current facts" 
576 
(K.tag_proof K.prf_decl) 

17900  577 
(Scan.succeed (Toplevel.proof' Calculation.moreover)); 
8562  578 

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

17068  581 
(K.tag_proof K.prf_chain) 
17900  582 
(Scan.succeed (Toplevel.proof' Calculation.ultimately)); 
8588  583 

6773  584 

6742  585 
(* proof navigation *) 
5944  586 

5832  587 
val backP = 
17068  588 
OuterSyntax.command "back" "backtracking of proof command" 
589 
(K.tag_proof K.prf_script) 

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

5832  591 

592 

6742  593 
(* history *) 
594 

595 
val cannot_undoP = 

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

9010  597 
(P.name >> (Toplevel.no_timing oo IsarCmd.cannot_undo)); 
6742  598 

7733  599 
val clear_undosP = 
600 
OuterSyntax.improper_command "clear_undos" "clear theorylevel undo information" K.control 

9010  601 
(P.nat >> (Toplevel.no_timing oo IsarCmd.clear_undos_theory)); 
6742  602 

603 
val redoP = 

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

9010  605 
(Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.redo)); 
6742  606 

607 
val undos_proofP = 

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

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

611 
val undoP = 

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

9010  613 
(Scan.succeed ((Toplevel.no_timing o Toplevel.print) o IsarCmd.undo)); 
6742  614 

8500  615 
val killP = 
616 
OuterSyntax.improper_command "kill" "kill current history node" K.control 

9010  617 
(Scan.succeed ((Toplevel.no_timing o Toplevel.print) o IsarCmd.kill)); 
8500  618 

6742  619 

5832  620 

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

622 

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

625 

7124  626 
val pretty_setmarginP = 
627 
OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing" 

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

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

5832  633 

7308  634 
val print_contextP = 
635 
OuterSyntax.improper_command "print_context" "print theory context name" K.diag 

9010  636 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_context)); 
7308  637 

5832  638 
val print_theoryP = 
6723  639 
OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag 
9010  640 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_theory)); 
5832  641 

642 
val print_syntaxP = 

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

5881  646 
val print_theoremsP = 
17068  647 
OuterSyntax.improper_command "print_theorems" 
648 
"print theorems of local theory or proof context" K.diag 

9010  649 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_theorems)); 
5881  650 

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

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

654 

655 
val print_localeP = 

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

12061  659 

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

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

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

15596  665 

5832  666 
val print_attributesP = 
12061  667 
OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag 
9010  668 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes)); 
5832  669 

16027  670 
val print_simpsetP = 
671 
OuterSyntax.improper_command "print_simpset" "print context of Simplifier" K.diag 

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

673 

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

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

677 

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

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

681 

9221  682 
val print_trans_rulesP = 
11666  683 
OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" K.diag 
9221  684 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules)); 
685 

5832  686 
val print_methodsP = 
12061  687 
OuterSyntax.improper_command "print_methods" "print methods of this theory" K.diag 
9010  688 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods)); 
5832  689 

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

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

693 

9454  694 
val thm_depsP = 
695 
OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies" 

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

697 

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

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

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

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

16074  703 
P.reserved "simp"  P.!!! (P.$$$ ":"  P.term) >> FindTheorems.Simp  
16027  704 
P.term >> FindTheorems.Pattern; 
705 

706 
val find_theoremsP = 

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

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

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

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

710 
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

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

712 

5832  713 
val print_bindsP = 
6723  714 
OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag 
9010  715 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds)); 
5832  716 

717 
val print_lthmsP = 

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

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

9010  723 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases)); 
8370  724 

5896  725 
val print_thmsP = 
8464  726 
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

727 
(opt_modes  P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms)); 
5832  728 

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

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

730 
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

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

732 

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

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

734 
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

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

736 

5832  737 
val print_propP = 
6723  738 
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

739 
(opt_modes  P.term >> (Toplevel.no_timing oo IsarCmd.print_prop)); 
5832  740 

741 
val print_termP = 

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

743 
(opt_modes  P.term >> (Toplevel.no_timing oo IsarCmd.print_term)); 
5832  744 

745 
val print_typeP = 

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

747 
(opt_modes  P.typ >> (Toplevel.no_timing oo IsarCmd.print_type)); 
5832  748 

749 

750 

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

752 

753 
val cdP = 

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

757 
val pwdP = 

6723  758 
OuterSyntax.improper_command "pwd" "print current working directory" K.diag 
9010  759 
(Scan.succeed (Toplevel.no_timing o IsarCmd.pwd)); 
5832  760 

761 
val use_thyP = 

6723  762 
OuterSyntax.improper_command "use_thy" "use theory file" K.diag 
9010  763 
(P.name >> (Toplevel.no_timing oo IsarCmd.use_thy)); 
5832  764 

6694  765 
val use_thy_onlyP = 
7102  766 
OuterSyntax.improper_command "use_thy_only" "use theory file only, ignoring associated ML" 
9010  767 
K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy_only)); 
6694  768 

6196  769 
val update_thyP = 
6723  770 
OuterSyntax.improper_command "update_thy" "update theory file" K.diag 
9010  771 
(P.name >> (Toplevel.no_timing oo IsarCmd.update_thy)); 
5832  772 

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

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

777 
val touch_thyP = 

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

9010  779 
(P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy)); 
7102  780 

781 
val touch_all_thysP = 

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

9010  783 
(Scan.succeed (Toplevel.no_timing o IsarCmd.touch_all_thys)); 
7102  784 

7908  785 
val touch_child_thysP = 
786 
OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag 

9010  787 
(P.name >> (Toplevel.no_timing oo IsarCmd.touch_child_thys)); 
7908  788 

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

9010  791 
(P.name >> (Toplevel.no_timing oo IsarCmd.remove_thy)); 
7102  792 

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

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

14934  797 
val display_draftsP = 
798 
OuterSyntax.improper_command "display_drafts" "display raw source files with symbols" 

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

801 
val print_draftsP = 

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

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

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

807 

5832  808 
val prP = 
8886  809 
OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag 
9731  810 
(opt_modes  opt_limits >> (Toplevel.no_timing oo IsarCmd.pr)); 
7199  811 

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

9010  814 
(Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr)); 
5832  815 

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

9010  818 
(Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr)); 
7222  819 

5832  820 
val commitP = 
6723  821 
OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag 
9010  822 
(P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.use_commit)); 
5832  823 

824 
val quitP = 

6723  825 
OuterSyntax.improper_command "quit" "quit Isabelle" K.control 
9010  826 
(P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit)); 
5832  827 

828 
val exitP = 

6723  829 
OuterSyntax.improper_command "exit" "exit Isar loop" K.control 
9010  830 
(Scan.succeed (Toplevel.no_timing o IsarCmd.exit)); 
5832  831 

7102  832 
val init_toplevelP = 
833 
OuterSyntax.improper_command "init_toplevel" "restart Isar toplevel loop" K.control 

9010  834 
(Scan.succeed (Toplevel.no_timing o IsarCmd.init_toplevel)); 
5991  835 

7462  836 
val welcomeP = 
8678  837 
OuterSyntax.improper_command "welcome" "print welcome message" K.diag 
9010  838 
(Scan.succeed (Toplevel.no_timing o IsarCmd.welcome)); 
7462  839 

5832  840 

841 

842 
(** the Pure outer syntax **) 

843 

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

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

846 

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

18822  850 
"begin", "binder", "concl", "constrains", "defines", "fixes", 
851 
"imports", "in", "includes", "infix", "infixl", "infixr", "is", 

852 
"notes", "open", "output", "overloaded", "shows", "structure", 

16264  853 
"uses", "where", "", "\\<equiv>", "\\<leftharpoondown>", 
854 
"\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>"]; 

5832  855 

16038  856 
val _ = OuterSyntax.add_parsers [ 
5832  857 
(*theory structure*) 
8500  858 
theoryP, end_excursionP, contextP, 
7775  859 
(*markup commands*) 
7733  860 
headerP, chapterP, sectionP, subsectionP, subsubsectionP, textP, 
7862  861 
text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP, 
5832  862 
(*theory sections*) 
7172  863 
classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP, 
15748  864 
aritiesP, judgmentP, constsP, finalconstsP, syntaxP, no_syntaxP, 
18780  865 
translationsP, axiomsP, defsP, constdefsP, definitionP, 
866 
axiomatizationP, theoremsP, lemmasP, declareP, globalP, localP, 

867 
hideP, useP, mlP, ml_commandP, ml_setupP, setupP, method_setupP, 

18616  868 
parse_ast_translationP, parse_translationP, print_translationP, 
869 
typed_print_translationP, print_ast_translationP, 

870 
token_translationP, oracleP, localeP, 

5832  871 
(*proof commands*) 
17353  872 
theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP, 
17854  873 
assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP, 
18544  874 
withP, noteP, usingP, unfoldingP, beginP, endP, nextP, qedP, 
875 
terminal_proofP, default_proofP, immediate_proofP, done_proofP, 

876 
skip_proofP, forget_proofP, deferP, preferP, applyP, apply_endP, 

877 
proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP, 

878 
cannot_undoP, clear_undosP, redoP, undos_proofP, undoP, killP, 

879 
interpretationP, interpretP, 

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

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

881 
pretty_setmarginP, 
16027  882 
print_commandsP, print_contextP, print_theoryP, print_syntaxP, 
883 
print_theoremsP, print_localesP, print_localeP, 

884 
print_registrationsP, print_attributesP, print_simpsetP, 

885 
print_rulesP, print_induct_rulesP, print_trans_rulesP, 

886 
print_methodsP, print_antiquotationsP, thm_depsP, find_theoremsP, 

887 
print_bindsP, print_lthmsP, print_casesP, print_thmsP, print_prfsP, 

888 
print_full_prfsP, print_propP, print_termP, print_typeP, 

5832  889 
(*system commands*) 
7102  890 
cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP, 
7931  891 
touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP, 
14934  892 
kill_thyP, display_draftsP, print_draftsP, prP, disable_prP, 
893 
enable_prP, commitP, quitP, exitP, init_toplevelP, welcomeP]; 

5832  894 

895 
end; 