author  wenzelm 
Wed, 11 Oct 2006 22:55:16 +0200  
changeset 20979  7e5ba4a1f72f 
parent 20958  802705101b2a 
child 21004  081674431d68 
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 

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

20979  22 
(Scan.succeed (Toplevel.exit o Toplevel.exit_local_theory)); 
6687  23 

6245  24 
val contextP = 
20958  25 
OuterSyntax.improper_command "context" "switch (local) theory context" 
26 
(K.tag_theory K.thy_switch) 

20979  27 
(P.name  P.begin >> (fn name => 
28 
Toplevel.print o IsarThy.context name o 

29 
Toplevel.begin_local_theory true (TheoryTarget.init (SOME name)))); 

5832  30 

31 

7749  32 
(** markup commands **) 
5832  33 

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

9129  37 
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

38 
K.thy_heading (P.opt_locale_target  P.position P.text >> IsarCmd.add_chapter); 
5958  39 

9129  40 
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

41 
K.thy_heading (P.opt_locale_target  P.position P.text >> IsarCmd.add_section); 
5958  42 

9129  43 
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

44 
K.thy_heading (P.opt_locale_target  P.position P.text >> IsarCmd.add_subsection); 
5958  45 

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

48 
K.thy_heading (P.opt_locale_target  P.position P.text >> IsarCmd.add_subsubsection); 
5832  49 

9129  50 
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

51 
K.thy_decl (P.opt_locale_target  P.position P.text >> IsarCmd.add_text); 
7172  52 

9129  53 
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

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

55 
K.thy_decl (P.position P.text >> IsarCmd.add_text_raw); 
7172  56 

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

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

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

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

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

5832  74 

6886  75 

76 
(** theory sections **) 

77 

5832  78 
(* classes and sorts *) 
79 

80 
val classesP = 

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

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

85 
val classrelP = 

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

90 
val defaultsortP = 

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

92 
(P.sort >> (Toplevel.theory o Theory.add_defsort)); 
5832  93 

19245  94 
val axclassP = 
95 
OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl 

96 
((P.name  Scan.optional ((P.$$$ "\\<subseteq>"  P.$$$ "<")  

19431
20e86336a53f
axclass: oldstyle concrete syntax for canonical specification format;
wenzelm
parents:
19410
diff
changeset

97 
P.!!! (P.list1 P.xname)) [])  
20e86336a53f
axclass: oldstyle concrete syntax for canonical specification format;
wenzelm
parents:
19410
diff
changeset

98 
Scan.repeat (P.thm_name ":"  (P.prop >> single)) 
19516  99 
>> (fn (x, y) => Toplevel.theory (snd o AxClass.define_class x [] y))); 
19245  100 

5832  101 

102 
(* types *) 

103 

104 
val typedeclP = 

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

106 
(P.type_args  P.name  P.opt_infix >> (fn ((args, a), mx) => 
16447  107 
Toplevel.theory (Theory.add_typedecls [(a, args, mx)]))); 
5832  108 

109 
val typeabbrP = 

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

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

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

114 
map (fn ((args, a), (T, mx)) => (a, args, T, mx)))); 
5832  115 

116 
val nontermP = 

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

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

120 
val aritiesP = 

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

122 
(Scan.repeat1 (P.xname  (P.$$$ "::"  P.!!! P.arity) >> P.triple2) 
19516  123 
>> (Toplevel.theory o fold AxClass.axiomatize_arity)); 
5832  124 

125 

126 
(* consts and syntax *) 

127 

8227  128 
val judgmentP = 
129 
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

130 
(P.const >> (Toplevel.theory o ObjectLogic.add_judgment)); 
8227  131 

5832  132 
val constsP = 
6723  133 
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

134 
(Scan.repeat1 P.const >> (Toplevel.theory o Theory.add_consts)); 
5832  135 

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

137 

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

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

139 
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

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

12142  142 
val mode_spec = 
9731  143 
(P.$$$ "output" >> K ("", false))  P.name  Scan.optional (P.$$$ "output" >> K false) true; 
144 

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

5832  147 

148 
val syntaxP = 

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

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

15748  152 
val no_syntaxP = 
153 
OuterSyntax.command "no_syntax" "delete syntax declarations" K.thy_decl 

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

155 

5832  156 

157 
(* translations *) 

158 

159 
val trans_pat = 

6723  160 
Scan.optional (P.$$$ "("  P.!!! (P.xname  P.$$$ ")")) "logic"  P.string; 
5832  161 

162 
fun trans_arrow toks = 

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

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

5832  166 

167 
val trans_line = 

6723  168 
trans_pat  P.!!! (trans_arrow  trans_pat) 
5832  169 
>> (fn (left, (arr, right)) => arr (left, right)); 
170 

171 
val translationsP = 

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

173 
(Scan.repeat1 trans_line >> (Toplevel.theory o Theory.add_trrules)); 
5832  174 

19260  175 
val no_translationsP = 
176 
OuterSyntax.command "no_translations" "remove syntax translation rules" K.thy_decl 

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

178 

5832  179 

180 
(* axioms and definitions *) 

181 

182 
val axiomsP = 

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

184 
(Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_axioms)); 
5832  185 

19631  186 
val opt_unchecked_overloaded = 
187 
Scan.optional (P.$$$ "("  P.!!! 

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

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

190 

5832  191 
val defsP = 
6723  192 
OuterSyntax.command "defs" "define constants" K.thy_decl 
19631  193 
(opt_unchecked_overloaded  Scan.repeat1 P.spec_name 
194 
>> (Toplevel.theory o IsarThy.add_defs)); 

6370  195 

14642  196 

19076  197 
(* constant definitions and abbreviations *) 
14642  198 

199 
val constdecl = 

18670  200 
(P.name  P.$$$ "where") >> (fn x => (x, NONE, NoSyn))  
19219  201 
P.name  (P.$$$ "::"  P.!!! P.typ >> SOME)  P.opt_mixfix' 
202 
 Scan.option (P.$$$ "where") >> P.triple1  

203 
P.name  (P.mixfix >> pair NONE)  Scan.option (P.$$$ "where") >> P.triple2; 

19076  204 

14642  205 
val constdef = Scan.option constdecl  (P.opt_thm_name ":"  P.prop); 
206 

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

209 

6370  210 
val constdefsP = 
19076  211 
OuterSyntax.command "constdefs" "oldstyle constant definition" K.thy_decl 
14642  212 
(structs  Scan.repeat1 constdef >> (Toplevel.theory o Constdefs.add_constdefs)); 
5832  213 

18780  214 
val definitionP = 
19076  215 
OuterSyntax.command "definition" "constant definition" K.thy_decl 
18780  216 
(P.opt_locale_target  Scan.repeat1 constdef 
18949  217 
>> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.definition args))); 
18780  218 

19076  219 
val abbreviationP = 
220 
OuterSyntax.command "abbreviation" "constant abbreviation" K.thy_decl 

19368  221 
(P.opt_locale_target  opt_mode  
19076  222 
Scan.repeat1 (Scan.option constdecl  P.prop) 
19659  223 
>> (fn ((loc, mode), args) => 
224 
Toplevel.local_theory loc (Specification.abbreviation mode args))); 

225 

226 
val const_syntaxP = 

227 
OuterSyntax.command "const_syntax" "constant syntax" K.thy_decl 

228 
(P.opt_locale_target  opt_mode  Scan.repeat1 (P.xname  P.mixfix) 

229 
>> (fn ((loc, mode), args) => 

230 
Toplevel.local_theory loc (Specification.const_syntax mode args))); 

19076  231 

5832  232 

18616  233 
(* constant specifications *) 
234 

235 
val axiomatizationP = 

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

18766  237 
(P.opt_locale_target  
18949  238 
(Scan.optional P.fixes []  
239 
Scan.optional (P.$$$ "where"  P.!!! (P.and_list1 P.spec)) []) 

240 
>> (fn (loc, (x, y)) => Toplevel.local_theory loc (#2 o Specification.axiomatization x y))); 

18616  241 

242 

5914  243 
(* theorems *) 
244 

17353  245 
fun theorems kind = P.opt_locale_target  P.name_facts 
20907  246 
>> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.theorems kind args)); 
12712  247 

5914  248 
val theoremsP = 
18799  249 
OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems PureThy.theoremK); 
5914  250 

251 
val lemmasP = 

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

9589  254 
val declareP = 
9776  255 
OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19431
diff
changeset

256 
(P.opt_locale_target  (P.and_list1 P.xthms1 >> flat) 
20907  257 
>> (fn (loc, args) => Toplevel.local_theory loc 
258 
(#2 o Specification.theorems "" [(("", []), args)]))); 

9589  259 

5914  260 

5832  261 
(* name space entry path *) 
262 

263 
val globalP = 

6723  264 
OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl 
16447  265 
(Scan.succeed (Toplevel.theory Sign.root_path)); 
5832  266 

267 
val localP = 

6723  268 
OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl 
16447  269 
(Scan.succeed (Toplevel.theory Sign.local_path)); 
8723  270 

271 
val hideP = 

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

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

5832  275 

276 

277 
(* use ML text *) 

278 

279 
val useP = 

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

283 
val mlP = 

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

285 
(P.text >> IsarCmd.use_mltext true); 
7891  286 

287 
val ml_commandP = 

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

289 
(P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false)); 
7616  290 

291 
val ml_setupP = 

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

293 
(P.text >> IsarCmd.use_mltext_theory); 
5832  294 

295 
val setupP = 

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

9197  299 
val method_setupP = 
17068  300 
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

301 
(((P.name  P.!!! (P.$$$ "="  P.text  P.text) >> P.triple2)) 
17353  302 
>> (Toplevel.theory o Method.method_setup)); 
9197  303 

5832  304 

305 
(* translation functions *) 

306 

14642  307 
val trfun = P.opt_keyword "advanced"  P.text; 
308 

5832  309 
val parse_ast_translationP = 
17068  310 
OuterSyntax.command "parse_ast_translation" "install parse ast translation functions" 
311 
(K.tag_ml K.thy_decl) 

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

312 
(trfun >> (Toplevel.theory o Sign.parse_ast_translation)); 
5832  313 

314 
val parse_translationP = 

17068  315 
OuterSyntax.command "parse_translation" "install parse translation functions" 
316 
(K.tag_ml K.thy_decl) 

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

317 
(trfun >> (Toplevel.theory o Sign.parse_translation)); 
5832  318 

319 
val print_translationP = 

17068  320 
OuterSyntax.command "print_translation" "install print translation functions" 
321 
(K.tag_ml K.thy_decl) 

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

322 
(trfun >> (Toplevel.theory o Sign.print_translation)); 
5832  323 

324 
val typed_print_translationP = 

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

327 
(trfun >> (Toplevel.theory o Sign.typed_print_translation)); 
5832  328 

329 
val print_ast_translationP = 

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

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

332 
(trfun >> (Toplevel.theory o Sign.print_ast_translation)); 
5832  333 

334 
val token_translationP = 

17068  335 
OuterSyntax.command "token_translation" "install token translation functions" 
336 
(K.tag_ml K.thy_decl) 

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

337 
(P.text >> (Toplevel.theory o Sign.token_translation)); 
5832  338 

339 

340 
(* oracles *) 

341 

342 
val oracleP = 

17068  343 
OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl) 
16849  344 
(P.name  (P.$$$ "("  P.text  P.$$$ ")"  P.$$$ "=") 
17353  345 
 P.text >> (Toplevel.theory o PureThy.add_oracle o P.triple1)); 
5832  346 

347 

12061  348 
(* locales *) 
349 

12758  350 
val locale_val = 
351 
(P.locale_expr  

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

12061  354 

355 
val localeP = 

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

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

20958  359 
 P.opt_begin 
360 
>> (fn (((is_open, name), (expr, elems)), begin) => 

20979  361 
Toplevel.begin_local_theory begin 
362 
(Locale.add_locale is_open name expr elems #> TheoryTarget.begin))); 

12061  363 

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

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

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

366 
"prove and register interpretation of locale expression in theory or locale" K.thy_goal 
17353  367 
(P.xname  (P.$$$ "\\<subseteq>"  P.$$$ "<")  P.!!! P.locale_expr 
20365  368 
>> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I))  
369 
P.opt_thm_name ":"  P.locale_expr  P.locale_insts >> (fn ((x, y), z) => 

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

12061  371 

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

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

373 
OuterSyntax.command "interpret" 
17068  374 
"prove and register interpretation of locale expression in proof context" 
375 
(K.tag_proof K.prf_goal) 

19809  376 
(P.opt_thm_name ":"  P.locale_expr  P.locale_insts >> (fn ((x, y), z) => 
20365  377 
Toplevel.print o Toplevel.proof' (Locale.interpret Seq.single x y z))); 
15703  378 

379 

5832  380 

381 
(** proof commands **) 

382 

383 
(* statements *) 

384 

17353  385 
fun gen_theorem kind = 
386 
OuterSyntax.command kind ("state " ^ kind) K.thy_goal 

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

387 
(P.opt_locale_target  Scan.optional (P.opt_thm_name ":"  
18895  388 
Scan.ahead (P.locale_keyword  P.statement_keyword)) ("", [])  
389 
P.general_statement >> (fn ((x, y), (z, w)) => 

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

18799  392 
val theoremP = gen_theorem PureThy.theoremK; 
393 
val lemmaP = gen_theorem PureThy.lemmaK; 

394 
val corollaryP = gen_theorem PureThy.corollaryK; 

5832  395 

17353  396 
val haveP = 
397 
OuterSyntax.command "have" "state local goal" 

398 
(K.tag_proof K.prf_goal) 

18895  399 
(P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.have)); 
17353  400 

401 
val henceP = 

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

403 
(K.tag_proof K.prf_goal) 

18895  404 
(P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.hence)); 
17353  405 

5832  406 
val showP = 
17068  407 
OuterSyntax.command "show" "state local goal, solving current obligation" 
408 
(K.tag_proof K.prf_goal) 

18895  409 
(P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.show)); 
5832  410 

6501  411 
val thusP = 
17068  412 
OuterSyntax.command "thus" "abbreviates \"then show\"" 
413 
(K.tag_proof K.prf_goal) 

18895  414 
(P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.thus)); 
6501  415 

5832  416 

5914  417 
(* facts *) 
5832  418 

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

419 
val facts = P.and_list1 P.xthms1; 
9197  420 

5832  421 
val thenP = 
17068  422 
OuterSyntax.command "then" "forward chaining" 
423 
(K.tag_proof K.prf_chain) 

17900  424 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain)); 
5832  425 

426 
val fromP = 

17068  427 
OuterSyntax.command "from" "forward chaining from given facts" 
428 
(K.tag_proof K.prf_chain) 

17900  429 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss))); 
5914  430 

6878  431 
val withP = 
17068  432 
OuterSyntax.command "with" "forward chaining from given and current facts" 
433 
(K.tag_proof K.prf_chain) 

17900  434 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss))); 
6878  435 

6773  436 
val noteP = 
17068  437 
OuterSyntax.command "note" "define facts" 
438 
(K.tag_proof K.prf_decl) 

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

12926  441 
val usingP = 
17068  442 
OuterSyntax.command "using" "augment goal facts" 
443 
(K.tag_proof K.prf_decl) 

18544  444 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.using))); 
445 

446 
val unfoldingP = 

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

448 
(K.tag_proof K.prf_decl) 

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

12926  450 

5832  451 

452 
(* proof context *) 

453 

11890  454 
val fixP = 
17068  455 
OuterSyntax.command "fix" "fix local variables (Skolem constants)" 
456 
(K.tag_proof K.prf_asm) 

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

5832  459 
val assumeP = 
17068  460 
OuterSyntax.command "assume" "assume propositions" 
461 
(K.tag_proof K.prf_asm) 

18895  462 
(P.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume))); 
5832  463 

6850  464 
val presumeP = 
17068  465 
OuterSyntax.command "presume" "assume propositions, to be established later" 
466 
(K.tag_proof K.prf_asm) 

18895  467 
(P.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume))); 
6850  468 

6953  469 
val defP = 
17068  470 
OuterSyntax.command "def" "local definition" 
471 
(K.tag_proof K.prf_asm) 

18308  472 
(P.and_list1 
19844  473 
(P.opt_thm_name ":"  
474 
((P.name  P.opt_mixfix)  ((P.$$$ "\\<equiv>"  P.$$$ "==")  P.!!! P.termp))) 

18308  475 
>> (Toplevel.print oo (Toplevel.proof o Proof.def))); 
6953  476 

11890  477 
val obtainP = 
478 
OuterSyntax.command "obtain" "generalized existence" 

17068  479 
(K.tag_proof K.prf_asm_goal) 
19844  480 
(P.parname  Scan.optional (P.fixes  P.$$$ "where") []  P.statement 
18895  481 
>> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain x y z))); 
5832  482 

17854  483 
val guessP = 
484 
OuterSyntax.command "guess" "wild guessing (unstructured)" 

485 
(K.tag_proof K.prf_asm_goal) 

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

5832  488 
val letP = 
17068  489 
OuterSyntax.command "let" "bind text variables" 
490 
(K.tag_proof K.prf_decl) 

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

491 
(P.and_list1 (P.enum1 "and" P.term  (P.$$$ "="  P.term)) 
17900  492 
>> (Toplevel.print oo (Toplevel.proof o Proof.let_bind))); 
5832  493 

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

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

497 

8370  498 
val caseP = 
17068  499 
OuterSyntax.command "case" "invoke local context" 
500 
(K.tag_proof K.prf_asm) 

17900  501 
(case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case))); 
8370  502 

5832  503 

504 
(* proof structure *) 

505 

20958  506 
val begin_blockP = 
17068  507 
OuterSyntax.command "{" "begin explicit proof block" 
508 
(K.tag_proof K.prf_open) 

17900  509 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block)); 
5832  510 

20958  511 
val end_blockP = 
17068  512 
OuterSyntax.command "}" "end explicit proof block" 
513 
(K.tag_proof K.prf_close) 

20305  514 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block)); 
6687  515 

5832  516 
val nextP = 
17068  517 
OuterSyntax.command "next" "enter next proof block" 
518 
(K.tag_proof K.prf_block) 

17900  519 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block)); 
5832  520 

521 

522 
(* end proof *) 

523 

6404  524 
val qedP = 
17068  525 
OuterSyntax.command "qed" "conclude (sub)proof" 
526 
(K.tag_proof K.qed_block) 

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

6404  529 
val terminal_proofP = 
17068  530 
OuterSyntax.command "by" "terminal backward proof" 
531 
(K.tag_proof K.qed) 

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

8966  534 
val default_proofP = 
17068  535 
OuterSyntax.command ".." "default proof" 
536 
(K.tag_proof K.qed) 

17353  537 
(Scan.succeed (Toplevel.print3 o IsarThy.default_proof)); 
8966  538 

6404  539 
val immediate_proofP = 
17068  540 
OuterSyntax.command "." "immediate proof" 
541 
(K.tag_proof K.qed) 

17353  542 
(Scan.succeed (Toplevel.print3 o IsarThy.immediate_proof)); 
6404  543 

8966  544 
val done_proofP = 
17068  545 
OuterSyntax.command "done" "done proof" 
546 
(K.tag_proof K.qed) 

17353  547 
(Scan.succeed (Toplevel.print3 o IsarThy.done_proof)); 
5832  548 

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

549 
val skip_proofP = 
17068  550 
OuterSyntax.improper_command "sorry" "skip proof (quickanddirty mode only!)" 
551 
(K.tag_proof K.qed) 

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

553 

8210  554 
val forget_proofP = 
17068  555 
OuterSyntax.command "oops" "forget proof" 
556 
(K.tag_proof K.qed_global) 

18561  557 
(Scan.succeed Toplevel.forget_proof); 
8210  558 

5832  559 

560 
(* proof steps *) 

561 

8165  562 
val deferP = 
17068  563 
OuterSyntax.command "defer" "shuffle internal proof state" 
564 
(K.tag_proof K.prf_script) 

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

567 
val preferP = 

17068  568 
OuterSyntax.command "prefer" "shuffle internal proof state" 
569 
(K.tag_proof K.prf_script) 

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

6850  572 
val applyP = 
17068  573 
OuterSyntax.command "apply" "initial refinement step (unstructured)" 
574 
(K.tag_proof K.prf_script) 

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

8235  577 
val apply_endP = 
17068  578 
OuterSyntax.command "apply_end" "terminal refinement (unstructured)" 
579 
(K.tag_proof K.prf_script) 

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

6404  582 
val proofP = 
17068  583 
OuterSyntax.command "proof" "backward proof" 
584 
(K.tag_proof K.prf_block) 

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

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

587 
Toplevel.skip_proof (History.apply (fn i => i + 1)))); 
5832  588 

589 

6773  590 
(* calculational proof commands *) 
591 

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

593 
Scan.option (P.$$$ "("  P.!!! ((P.xthms1  P.$$$ ")"))); 
6878  594 

6773  595 
val alsoP = 
17068  596 
OuterSyntax.command "also" "combine calculation and current facts" 
597 
(K.tag_proof K.prf_decl) 

17900  598 
(calc_args >> (Toplevel.proofs' o Calculation.also)); 
6773  599 

600 
val finallyP = 

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

17900  603 
(calc_args >> (Toplevel.proofs' o Calculation.finally)); 
6773  604 

8562  605 
val moreoverP = 
17068  606 
OuterSyntax.command "moreover" "augment calculation by current facts" 
607 
(K.tag_proof K.prf_decl) 

17900  608 
(Scan.succeed (Toplevel.proof' Calculation.moreover)); 
8562  609 

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

17068  612 
(K.tag_proof K.prf_chain) 
17900  613 
(Scan.succeed (Toplevel.proof' Calculation.ultimately)); 
8588  614 

6773  615 

6742  616 
(* proof navigation *) 
5944  617 

5832  618 
val backP = 
17068  619 
OuterSyntax.command "back" "backtracking of proof command" 
620 
(K.tag_proof K.prf_script) 

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

5832  622 

623 

6742  624 
(* history *) 
625 

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

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

6742  629 

7733  630 
val clear_undosP = 
631 
OuterSyntax.improper_command "clear_undos" "clear theorylevel undo information" K.control 

9010  632 
(P.nat >> (Toplevel.no_timing oo IsarCmd.clear_undos_theory)); 
6742  633 

634 
val redoP = 

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

9010  636 
(Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.redo)); 
6742  637 

638 
val undos_proofP = 

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

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

642 
val undoP = 

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

9010  644 
(Scan.succeed ((Toplevel.no_timing o Toplevel.print) o IsarCmd.undo)); 
6742  645 

8500  646 
val killP = 
647 
OuterSyntax.improper_command "kill" "kill current history node" K.control 

9010  648 
(Scan.succeed ((Toplevel.no_timing o Toplevel.print) o IsarCmd.kill)); 
8500  649 

6742  650 

5832  651 

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

653 

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

7124  657 
val pretty_setmarginP = 
658 
OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing" 

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

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

5832  664 

7308  665 
val print_contextP = 
666 
OuterSyntax.improper_command "print_context" "print theory context name" K.diag 

9010  667 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_context)); 
7308  668 

5832  669 
val print_theoryP = 
6723  670 
OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag 
20621  671 
(opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory)); 
5832  672 

673 
val print_syntaxP = 

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

5881  677 
val print_theoremsP = 
17068  678 
OuterSyntax.improper_command "print_theorems" 
679 
"print theorems of local theory or proof context" K.diag 

9010  680 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_theorems)); 
5881  681 

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

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

685 

686 
val print_localeP = 

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

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

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

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

15596  695 

5832  696 
val print_attributesP = 
12061  697 
OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag 
9010  698 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes)); 
5832  699 

16027  700 
val print_simpsetP = 
701 
OuterSyntax.improper_command "print_simpset" "print context of Simplifier" K.diag 

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

703 

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

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

707 

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

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

711 

9221  712 
val print_trans_rulesP = 
11666  713 
OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" K.diag 
9221  714 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules)); 
715 

5832  716 
val print_methodsP = 
12061  717 
OuterSyntax.improper_command "print_methods" "print methods of this theory" K.diag 
9010  718 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods)); 
5832  719 

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

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

723 

20574  724 
val class_depsP = 
725 
OuterSyntax.improper_command "class_deps" "visualize class dependencies" 

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

727 

9454  728 
val thm_depsP = 
729 
OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies" 

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

731 

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

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

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

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

16074  737 
P.reserved "simp"  P.!!! (P.$$$ ":"  P.term) >> FindTheorems.Simp  
16027  738 
P.term >> FindTheorems.Pattern; 
739 

740 
val find_theoremsP = 

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

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

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

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

744 
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

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

746 

5832  747 
val print_bindsP = 
6723  748 
OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag 
9010  749 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds)); 
5832  750 

751 
val print_lthmsP = 

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

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

9010  757 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases)); 
8370  758 

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

761 
(opt_modes  P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts)); 

762 

5896  763 
val print_thmsP = 
8464  764 
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

765 
(opt_modes  P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms)); 
5832  766 

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

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

768 
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

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

770 

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

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

772 
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

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

774 

5832  775 
val print_propP = 
6723  776 
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

777 
(opt_modes  P.term >> (Toplevel.no_timing oo IsarCmd.print_prop)); 
5832  778 

779 
val print_termP = 

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

781 
(opt_modes  P.term >> (Toplevel.no_timing oo IsarCmd.print_term)); 
5832  782 

783 
val print_typeP = 

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

785 
(opt_modes  P.typ >> (Toplevel.no_timing oo IsarCmd.print_type)); 
5832  786 

787 

788 

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

790 

791 
val cdP = 

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

795 
val pwdP = 

6723  796 
OuterSyntax.improper_command "pwd" "print current working directory" K.diag 
9010  797 
(Scan.succeed (Toplevel.no_timing o IsarCmd.pwd)); 
5832  798 

799 
val use_thyP = 

6723  800 
OuterSyntax.improper_command "use_thy" "use theory file" K.diag 
9010  801 
(P.name >> (Toplevel.no_timing oo IsarCmd.use_thy)); 
5832  802 

6694  803 
val use_thy_onlyP = 
7102  804 
OuterSyntax.improper_command "use_thy_only" "use theory file only, ignoring associated ML" 
9010  805 
K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy_only)); 
6694  806 

6196  807 
val update_thyP = 
6723  808 
OuterSyntax.improper_command "update_thy" "update theory file" K.diag 
9010  809 
(P.name >> (Toplevel.no_timing oo IsarCmd.update_thy)); 
5832  810 

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

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

815 
val touch_thyP = 

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

9010  817 
(P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy)); 
7102  818 

819 
val touch_all_thysP = 

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

9010  821 
(Scan.succeed (Toplevel.no_timing o IsarCmd.touch_all_thys)); 
7102  822 

7908  823 
val touch_child_thysP = 
824 
OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag 

9010  825 
(P.name >> (Toplevel.no_timing oo IsarCmd.touch_child_thys)); 
7908  826 

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

9010  829 
(P.name >> (Toplevel.no_timing oo IsarCmd.remove_thy)); 
7102  830 

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

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

14934  835 
val display_draftsP = 
836 
OuterSyntax.improper_command "display_drafts" "display raw source files with symbols" 

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

839 
val print_draftsP = 

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

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

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

845 

5832  846 
val prP = 
8886  847 
OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag 
9731  848 
(opt_modes  opt_limits >> (Toplevel.no_timing oo IsarCmd.pr)); 
7199  849 

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

9010  852 
(Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr)); 
5832  853 

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

9010  856 
(Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr)); 
7222  857 

5832  858 
val commitP = 
6723  859 
OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag 
9010  860 
(P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.use_commit)); 
5832  861 

862 
val quitP = 

6723  863 
OuterSyntax.improper_command "quit" "quit Isabelle" K.control 
9010  864 
(P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit)); 
5832  865 

866 
val exitP = 

6723  867 
OuterSyntax.improper_command "exit" "exit Isar loop" K.control 
9010  868 
(Scan.succeed (Toplevel.no_timing o IsarCmd.exit)); 
5832  869 

7102  870 
val init_toplevelP = 
871 
OuterSyntax.improper_command "init_toplevel" "restart Isar toplevel loop" K.control 

9010  872 
(Scan.succeed (Toplevel.no_timing o IsarCmd.init_toplevel)); 
5991  873 

7462  874 
val welcomeP = 
8678  875 
OuterSyntax.improper_command "welcome" "print welcome message" K.diag 
9010  876 
(Scan.succeed (Toplevel.no_timing o IsarCmd.welcome)); 
7462  877 

5832  878 

879 

880 
(** the Pure outer syntax **) 

881 

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

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

884 

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

19809  888 
"begin", "binder", "concl", "constrains", "defines", "fixes", "for", 
889 
"imports", "if", "in", "includes", "infix", "infixl", "infixr", 

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

19631  891 
"structure", "unchecked", "uses", "where", "", "\\<equiv>", 
18895  892 
"\\<leftharpoondown>", "\\<rightharpoonup>", 
893 
"\\<rightleftharpoons>", "\\<subseteq>"]; 

5832  894 

16038  895 
val _ = OuterSyntax.add_parsers [ 
5832  896 
(*theory structure*) 
20958  897 
theoryP, endP, contextP, 
7775  898 
(*markup commands*) 
7733  899 
headerP, chapterP, sectionP, subsectionP, subsubsectionP, textP, 
7862  900 
text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP, 
5832  901 
(*theory sections*) 
19245  902 
classesP, classrelP, defaultsortP, axclassP, typedeclP, typeabbrP, 
903 
nontermP, aritiesP, judgmentP, constsP, finalconstsP, syntaxP, 

19260  904 
no_syntaxP, translationsP, no_translationsP, axiomsP, defsP, 
19659  905 
constdefsP, definitionP, abbreviationP, const_syntaxP, 
906 
axiomatizationP, theoremsP, lemmasP, declareP, globalP, localP, 

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

908 
parse_ast_translationP, parse_translationP, print_translationP, 

909 
typed_print_translationP, print_ast_translationP, 

910 
token_translationP, oracleP, localeP, 

5832  911 
(*proof commands*) 
17353  912 
theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP, 
17854  913 
assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP, 
20958  914 
withP, noteP, usingP, unfoldingP, begin_blockP, end_blockP, nextP, 
915 
qedP, terminal_proofP, default_proofP, immediate_proofP, 

916 
done_proofP, skip_proofP, forget_proofP, deferP, preferP, applyP, 

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

20979  918 
cannot_undoP, clear_undosP, redoP, undos_proofP, undoP, killP, 
919 
interpretationP, interpretP, 

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

920 
(*diagnostic commands*) 
19269  921 
pretty_setmarginP, print_commandsP, print_contextP, print_theoryP, 
922 
print_syntaxP, print_theoremsP, print_localesP, print_localeP, 

16027  923 
print_registrationsP, print_attributesP, print_simpsetP, 
924 
print_rulesP, print_induct_rulesP, print_trans_rulesP, 

20574  925 
print_methodsP, print_antiquotationsP, class_depsP, thm_depsP, 
926 
find_theoremsP, print_bindsP, print_lthmsP, print_casesP, 

927 
print_stmtsP, print_thmsP, print_prfsP, print_full_prfsP, 

928 
print_propP, print_termP, print_typeP, 

5832  929 
(*system commands*) 
7102  930 
cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP, 
7931  931 
touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP, 
14934  932 
kill_thyP, display_draftsP, print_draftsP, prP, disable_prP, 
933 
enable_prP, commitP, quitP, exitP, init_toplevelP, welcomeP]; 

5832  934 

935 
end; 