author  wenzelm 
Sat, 24 May 2008 22:04:52 +0200  
changeset 26988  742e26213212 
parent 26888  9942cd184c48 
child 27113  ac87245d8cab 
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 

24868  14 
(** keywords **) 
15 

16 
(*keep keywords consistent with the parsers, otherwise be prepared for 

17 
unexpected errors*) 

18 

19 
val _ = OuterSyntax.keywords 

20 
["!!", "!", "%", "(", ")", "+", ",", "", ":", "::", ";", "<", "<=", 

21 
"=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>", 

22 
"\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]", 

26888  23 
"advanced", "and", "assumes", "attach", "begin", "binder", 
24868  24 
"constrains", "defines", "fixes", "for", "identifier", "if", 
25 
"imports", "in", "includes", "infix", "infixl", "infixr", "is", 

25003  26 
"notes", "obtains", "open", "output", "overloaded", "shows", 
24868  27 
"structure", "unchecked", "uses", "where", ""]; 
28 

29 

5832  30 
(** init and exit **) 
31 

24868  32 
val _ = 
17068  33 
OuterSyntax.command "theory" "begin theory" (K.tag_theory K.thy_begin) 
21350  34 
(ThyHeader.args >> (Toplevel.print oo IsarCmd.theory)); 
5832  35 

24868  36 
val _ = 
20958  37 
OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end) 
21004  38 
(Scan.succeed (Toplevel.exit o Toplevel.end_local_theory)); 
6687  39 

5832  40 

7749  41 
(** markup commands **) 
5832  42 

24868  43 
val _ = OuterSyntax.markup_command ThyOutput.Markup "header" "theory header" K.diag 
12940  44 
(P.position P.text >> IsarCmd.add_header); 
6353  45 

24868  46 
val _ = OuterSyntax.markup_command ThyOutput.Markup "chapter" "chapter heading" 
22117  47 
K.thy_heading (P.opt_target  P.position P.text >> IsarCmd.add_chapter); 
5958  48 

24868  49 
val _ = OuterSyntax.markup_command ThyOutput.Markup "section" "section heading" 
22117  50 
K.thy_heading (P.opt_target  P.position P.text >> IsarCmd.add_section); 
5958  51 

24868  52 
val _ = OuterSyntax.markup_command ThyOutput.Markup "subsection" "subsection heading" 
22117  53 
K.thy_heading (P.opt_target  P.position P.text >> IsarCmd.add_subsection); 
5958  54 

24868  55 
val _ = 
22117  56 
OuterSyntax.markup_command ThyOutput.Markup "subsubsection" "subsubsection heading" 
57 
K.thy_heading (P.opt_target  P.position P.text >> IsarCmd.add_subsubsection); 

5832  58 

24868  59 
val _ = OuterSyntax.markup_command ThyOutput.MarkupEnv "text" "formal comment (theory)" 
22117  60 
K.thy_decl (P.opt_target  P.position P.text >> IsarCmd.add_text); 
7172  61 

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

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

64 
K.thy_decl (P.position P.text >> IsarCmd.add_text_raw); 
7172  65 

24868  66 
val _ = OuterSyntax.markup_command ThyOutput.Markup "sect" "formal comment (proof)" 
17068  67 
(K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.add_sect); 
7172  68 

24868  69 
val _ = OuterSyntax.markup_command ThyOutput.Markup "subsect" "formal comment (proof)" 
17068  70 
(K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.add_subsect); 
7172  71 

24868  72 
val _ = OuterSyntax.markup_command ThyOutput.Markup "subsubsect" 
17068  73 
"formal comment (proof)" (K.tag_proof K.prf_heading) 
12940  74 
(P.position P.text >> IsarCmd.add_subsubsect); 
7172  75 

24868  76 
val _ = OuterSyntax.markup_command ThyOutput.MarkupEnv "txt" "formal comment (proof)" 
17068  77 
(K.tag_proof K.prf_decl) (P.position P.text >> IsarCmd.add_txt); 
7172  78 

24868  79 
val _ = OuterSyntax.markup_command ThyOutput.Verbatim "txt_raw" 
17068  80 
"raw document preparation text (proof)" (K.tag_proof K.prf_decl) 
12940  81 
(P.position P.text >> IsarCmd.add_txt_raw); 
7775  82 

5832  83 

6886  84 

85 
(** theory sections **) 

86 

5832  87 
(* classes and sorts *) 
88 

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

91 
(Scan.repeat1 (P.name  Scan.optional ((P.$$$ "\\<subseteq>"  P.$$$ "<")  
24932
86ef9a828a9e
AxClass.axiomatize and Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
wenzelm
parents:
24914
diff
changeset

92 
P.!!! (P.list1 P.xname)) []) >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd)); 
5832  93 

24868  94 
val _ = 
6723  95 
OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl 
14779  96 
(P.and_list1 (P.xname  ((P.$$$ "\\<subseteq>"  P.$$$ "<")  P.!!! P.xname)) 
24932
86ef9a828a9e
AxClass.axiomatize and Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
wenzelm
parents:
24914
diff
changeset

97 
>> (Toplevel.theory o AxClass.axiomatize_classrel_cmd)); 
5832  98 

24868  99 
val _ = 
6723  100 
OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl 
22796  101 
(P.sort >> (Toplevel.theory o Sign.add_defsort)); 
5832  102 

24868  103 
val _ = 
19245  104 
OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl 
21462
74ddf3a522f8
added Isar syntax for adding parameters to axclasses
haftmann
parents:
21437
diff
changeset

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

106 
P.!!! (P.list1 P.xname)) [] 
22117  107 
 Scan.repeat (SpecParse.thm_name ":"  (P.prop >> single)) 
24219  108 
>> (fn (x, y) => Toplevel.theory (snd o Class.axclass_cmd x y))); 
19245  109 

5832  110 

111 
(* types *) 

112 

24868  113 
val _ = 
12624  114 
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

115 
(P.type_args  P.name  P.opt_infix >> (fn ((args, a), mx) => 
25495  116 
Toplevel.theory (ObjectLogic.typedecl (a, args, mx) #> snd))); 
5832  117 

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

121 
(P.type_args  P.name  (P.$$$ "="  P.!!! (P.typ  P.opt_infix'))) 
22796  122 
>> (Toplevel.theory o Sign.add_tyabbrs o 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

123 
map (fn ((args, a), (T, mx)) => (a, args, T, mx)))); 
5832  124 

24868  125 
val _ = 
6370  126 
OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols" 
22796  127 
K.thy_decl (Scan.repeat1 P.name >> (Toplevel.theory o Sign.add_nonterminals)); 
5832  128 

24868  129 
val _ = 
6723  130 
OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl 
24932
86ef9a828a9e
AxClass.axiomatize and Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
wenzelm
parents:
24914
diff
changeset

131 
(Scan.repeat1 P.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity_cmd)); 
5832  132 

133 

134 
(* consts and syntax *) 

135 

24868  136 
val _ = 
8227  137 
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

138 
(P.const >> (Toplevel.theory o ObjectLogic.add_judgment)); 
8227  139 

24868  140 
val _ = 
6723  141 
OuterSyntax.command "consts" "declare constants" K.thy_decl 
22796  142 
(Scan.repeat1 P.const >> (Toplevel.theory o Sign.add_consts)); 
5832  143 

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

145 

24868  146 
val _ = 
14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
13802
diff
changeset

147 
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

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

12142  150 
val mode_spec = 
9731  151 
(P.$$$ "output" >> K ("", false))  P.name  Scan.optional (P.$$$ "output" >> K false) true; 
152 

14900  153 
val opt_mode = 
24960  154 
Scan.optional (P.$$$ "("  P.!!! (mode_spec  P.$$$ ")")) Syntax.mode_default; 
5832  155 

24868  156 
val _ = 
6723  157 
OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl 
22796  158 
(opt_mode  Scan.repeat1 P.const >> (Toplevel.theory o uncurry Sign.add_modesyntax)); 
5832  159 

24868  160 
val _ = 
15748  161 
OuterSyntax.command "no_syntax" "delete syntax declarations" K.thy_decl 
22796  162 
(opt_mode  Scan.repeat1 P.const >> (Toplevel.theory o uncurry Sign.del_modesyntax)); 
15748  163 

5832  164 

165 
(* translations *) 

166 

167 
val trans_pat = 

6723  168 
Scan.optional (P.$$$ "("  P.!!! (P.xname  P.$$$ ")")) "logic"  P.string; 
5832  169 

170 
fun trans_arrow toks = 

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

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

5832  174 

175 
val trans_line = 

6723  176 
trans_pat  P.!!! (trans_arrow  trans_pat) 
5832  177 
>> (fn (left, (arr, right)) => arr (left, right)); 
178 

24868  179 
val _ = 
6723  180 
OuterSyntax.command "translations" "declare syntax translation rules" K.thy_decl 
22796  181 
(Scan.repeat1 trans_line >> (Toplevel.theory o Sign.add_trrules)); 
5832  182 

24868  183 
val _ = 
19260  184 
OuterSyntax.command "no_translations" "remove syntax translation rules" K.thy_decl 
22796  185 
(Scan.repeat1 trans_line >> (Toplevel.theory o Sign.del_trrules)); 
19260  186 

5832  187 

188 
(* axioms and definitions *) 

189 

24868  190 
val _ = 
6723  191 
OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl 
22117  192 
(Scan.repeat1 SpecParse.spec_name >> (Toplevel.theory o IsarCmd.add_axioms)); 
5832  193 

19631  194 
val opt_unchecked_overloaded = 
195 
Scan.optional (P.$$$ "("  P.!!! 

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

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

198 

24868  199 
val _ = 
6723  200 
OuterSyntax.command "defs" "define constants" K.thy_decl 
22117  201 
(opt_unchecked_overloaded  Scan.repeat1 SpecParse.spec_name 
21350  202 
>> (Toplevel.theory o IsarCmd.add_defs)); 
6370  203 

14642  204 

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

205 
(* old constdefs *) 
14642  206 

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

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

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

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

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

211 
P.name  (P.mixfix >> pair NONE)  Scan.option P.where_ >> P.triple2; 
19076  212 

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

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

217 

24868  218 
val _ = 
19076  219 
OuterSyntax.command "constdefs" "oldstyle constant definition" K.thy_decl 
21601
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

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

221 

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

222 

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

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

224 

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

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

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

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

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

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

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

231 

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

24868  234 
val _ = 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

235 
OuterSyntax.local_theory "definition" "constant definition" K.thy_decl 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

236 
(constdef >> (fn args => #2 o Specification.definition_cmd args)); 
18780  237 

24868  238 
val _ = 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

239 
OuterSyntax.local_theory "abbreviation" "constant abbreviation" K.thy_decl 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

240 
(opt_mode  (Scan.option constdecl  P.prop) 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

241 
>> (fn (mode, args) => Specification.abbreviation_cmd mode args)); 
19659  242 

24868  243 
val _ = 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

244 
OuterSyntax.local_theory "notation" "add notation for constants / fixed variables" K.thy_decl 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

245 
(opt_mode  P.and_list1 (P.xname  SpecParse.locale_mixfix) 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

246 
>> (fn (mode, args) => Specification.notation_cmd true mode args)); 
24950  247 

248 
val _ = 

26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

249 
OuterSyntax.local_theory "no_notation" "delete notation for constants / fixed variables" K.thy_decl 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

250 
(opt_mode  P.and_list1 (P.xname  SpecParse.locale_mixfix) 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

251 
>> (fn (mode, args) => Specification.notation_cmd false mode args)); 
19076  252 

5832  253 

18616  254 
(* constant specifications *) 
255 

24868  256 
val _ = 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

257 
OuterSyntax.local_theory "axiomatization" "axiomatic constant specification" K.thy_decl 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

258 
(Scan.optional P.fixes []  
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

259 
Scan.optional (P.where_  P.!!! (P.and_list1 SpecParse.spec)) [] 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

260 
>> (fn (x, y) => #2 o Specification.axiomatization_cmd x y)); 
18616  261 

262 

5914  263 
(* theorems *) 
264 

26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

265 
fun theorems kind = 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

266 
SpecParse.name_facts >> (fn args => #2 o Specification.theorems_cmd kind args); 
12712  267 

24868  268 
val _ = 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

269 
OuterSyntax.local_theory "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK); 
5914  270 

24868  271 
val _ = 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

272 
OuterSyntax.local_theory "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK); 
5914  273 

24868  274 
val _ = 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

275 
OuterSyntax.local_theory "declare" "declare theorems (improper)" K.thy_decl 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

276 
(P.and_list1 SpecParse.xthms1 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

277 
>> (fn args => #2 o Specification.theorems_cmd "" [(("", []), flat args)])); 
9589  278 

5914  279 

5832  280 
(* name space entry path *) 
281 

24868  282 
val _ = 
6723  283 
OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl 
16447  284 
(Scan.succeed (Toplevel.theory Sign.root_path)); 
5832  285 

24868  286 
val _ = 
6723  287 
OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl 
16447  288 
(Scan.succeed (Toplevel.theory Sign.local_path)); 
8723  289 

24868  290 
val _ = 
8723  291 
OuterSyntax.command "hide" "hide names from given name space" K.thy_decl 
17397  292 
((P.opt_keyword "open" >> not)  (P.name  Scan.repeat1 P.xname) >> 
26672  293 
(Toplevel.theory o uncurry IsarCmd.hide_names)); 
5832  294 

295 

296 
(* use ML text *) 

297 

24868  298 
val _ = 
26490  299 
OuterSyntax.command "use" "eval ML text from file" (K.tag_ml K.thy_decl) 
300 
(P.path >> (Toplevel.generic_theory o ThyInfo.exec_file false)); 

5832  301 

24868  302 
val _ = 
26490  303 
OuterSyntax.command "ML" "eval ML text (diagnostic)" (K.tag_ml K.thy_decl) 
304 
(P.position P.text >> (fn (txt, pos) => 

305 
Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt)))); 

7891  306 

24868  307 
val _ = 
26396  308 
OuterSyntax.command "ML_val" "eval ML text (diagnostic)" (K.tag_ml K.diag) 
26490  309 
(P.position P.text >> IsarCmd.ml_diag true); 
26396  310 

311 
val _ = 

312 
OuterSyntax.command "ML_command" "silently eval ML text (diagnostic)" (K.tag_ml K.diag) 

26490  313 
(P.position P.text >> (Toplevel.no_timing oo IsarCmd.ml_diag false)); 
5832  314 

24868  315 
val _ = 
17068  316 
OuterSyntax.command "setup" "apply ML theory setup" (K.tag_ml K.thy_decl) 
26435  317 
(P.position P.text >> (Toplevel.theory o IsarCmd.generic_setup)); 
5832  318 

24868  319 
val _ = 
17068  320 
OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl) 
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26248
diff
changeset

321 
(P.name  P.!!! (P.$$$ "="  P.position P.text  P.text) 
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26248
diff
changeset

322 
>> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt))); 
9197  323 

24868  324 
val _ = 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

325 
OuterSyntax.local_theory "declaration" "generic ML declaration" (K.tag_ml K.thy_decl) 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

326 
(P.position P.text >> IsarCmd.declaration); 
22088  327 

24868  328 
val _ = 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

329 
OuterSyntax.local_theory "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl) 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

330 
(P.name  (P.$$$ "("  P.enum1 "" P.term  P.$$$ ")"  P.$$$ "=")  
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26248
diff
changeset

331 
P.position P.text  Scan.optional (P.$$$ "identifier"  Scan.repeat1 P.xname) [] 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

332 
>> (fn (((a, b), c), d) => IsarCmd.simproc_setup a b c d)); 
22202  333 

5832  334 

335 
(* translation functions *) 

336 

26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26248
diff
changeset

337 
val trfun = P.opt_keyword "advanced"  P.position P.text; 
14642  338 

24868  339 
val _ = 
17068  340 
OuterSyntax.command "parse_ast_translation" "install parse ast translation functions" 
341 
(K.tag_ml K.thy_decl) 

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

24868  344 
val _ = 
17068  345 
OuterSyntax.command "parse_translation" "install parse translation functions" 
346 
(K.tag_ml K.thy_decl) 

22117  347 
(trfun >> (Toplevel.theory o IsarCmd.parse_translation)); 
5832  348 

24868  349 
val _ = 
17068  350 
OuterSyntax.command "print_translation" "install print translation functions" 
351 
(K.tag_ml K.thy_decl) 

22117  352 
(trfun >> (Toplevel.theory o IsarCmd.print_translation)); 
5832  353 

24868  354 
val _ = 
6370  355 
OuterSyntax.command "typed_print_translation" "install typed print translation functions" 
17068  356 
(K.tag_ml K.thy_decl) 
22117  357 
(trfun >> (Toplevel.theory o IsarCmd.typed_print_translation)); 
5832  358 

24868  359 
val _ = 
17068  360 
OuterSyntax.command "print_ast_translation" "install print ast translation functions" 
361 
(K.tag_ml K.thy_decl) 

22117  362 
(trfun >> (Toplevel.theory o IsarCmd.print_ast_translation)); 
5832  363 

24868  364 
val _ = 
17068  365 
OuterSyntax.command "token_translation" "install token translation functions" 
366 
(K.tag_ml K.thy_decl) 

26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26248
diff
changeset

367 
(P.position P.text >> (Toplevel.theory o IsarCmd.token_translation)); 
5832  368 

369 

370 
(* oracles *) 

371 

24868  372 
val _ = 
17068  373 
OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl) 
16849  374 
(P.name  (P.$$$ "("  P.text  P.$$$ ")"  P.$$$ "=") 
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26248
diff
changeset

375 
 P.position P.text >> (fn ((x, y), z) => Toplevel.theory (IsarCmd.oracle x y z))); 
5832  376 

377 

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

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

379 

24868  380 
val _ = 
21306
7ab6e95e6b0b
turned 'context' into plain thy_decl, discontinued thy_switch;
wenzelm
parents:
21269
diff
changeset

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

382 
(P.name  P.begin >> (fn name => 
25290  383 
Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.context name))); 
21306
7ab6e95e6b0b
turned 'context' into plain thy_decl, discontinued thy_switch;
wenzelm
parents:
21269
diff
changeset

384 

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

385 

12061  386 
(* locales *) 
387 

12758  388 
val locale_val = 
24868  389 
SpecParse.locale_expr  
22117  390 
Scan.optional (P.$$$ "+"  P.!!! (Scan.repeat1 SpecParse.context_element)) []  
24868  391 
Scan.repeat1 SpecParse.context_element >> pair Locale.empty; 
12061  392 

24868  393 
val _ = 
12061  394 
OuterSyntax.command "locale" "define named proof context" K.thy_decl 
24868  395 
((P.opt_keyword "open" >> (fn true => NONE  false => SOME ""))  
396 
P.name  Scan.optional (P.$$$ "="  P.!!! locale_val) (Locale.empty, [])  P.opt_begin 

20958  397 
>> (fn (((is_open, name), (expr, elems)), begin) => 
21843  398 
(begin ? Toplevel.print) o Toplevel.begin_local_theory begin 
22351
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports nonmandatory prefixes
haftmann
parents:
22340
diff
changeset

399 
(Locale.add_locale is_open name expr elems #> TheoryTarget.begin))); 
12061  400 

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

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

403 
"prove and register interpretation of locale expression in theory or locale" K.thy_goal 
22117  404 
(P.xname  (P.$$$ "\\<subseteq>"  P.$$$ "<")  P.!!! SpecParse.locale_expr 
20365  405 
>> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I))  
22866  406 
SpecParse.opt_thm_name ":"  SpecParse.locale_expr  SpecParse.locale_insts 
407 
>> (fn ((x, y), z) => Toplevel.print o 

408 
Toplevel.theory_to_proof (Locale.interpretation I (apfst (pair true) x) y z))); 

12061  409 

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

411 
OuterSyntax.command "interpret" 
17068  412 
"prove and register interpretation of locale expression in proof context" 
413 
(K.tag_proof K.prf_goal) 

22117  414 
(SpecParse.opt_thm_name ":"  SpecParse.locale_expr  SpecParse.locale_insts 
22866  415 
>> (fn ((x, y), z) => Toplevel.print o 
416 
Toplevel.proof' (Locale.interpret Seq.single (apfst (pair true) x) y z))); 

15703  417 

418 

22299  419 
(* classes *) 
420 

24868  421 
val class_val = 
422 
SpecParse.class_expr  

26248  423 
Scan.optional (P.$$$ "+"  P.!!! (Scan.repeat1 SpecParse.context_element)) []  
424 
Scan.repeat1 SpecParse.context_element >> pair []; 

22299  425 

24868  426 
val _ = 
427 
OuterSyntax.command "class" "define type class" K.thy_decl 

26516  428 
(P.name  (P.$$$ "="  class_val)  P.opt_begin 
429 
>> (fn ((name, (supclasses, elems)), begin) => 

24938  430 
(begin ? Toplevel.print) o Toplevel.begin_local_theory begin 
26516  431 
(Class.class_cmd name supclasses elems #> TheoryTarget.begin))); 
22299  432 

24868  433 
val _ = 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

434 
OuterSyntax.local_theory_to_proof "subclass" "prove a subclass relation" K.thy_goal 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

435 
(P.xname >> Subclass.subclass_cmd); 
24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24871
diff
changeset

436 

95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24871
diff
changeset

437 
val _ = 
25519  438 
OuterSyntax.command "instantiation" "instantiate and prove type arity" K.thy_decl 
25536  439 
(P.multi_arity  P.begin 
25462  440 
>> (fn arities => Toplevel.print o 
441 
Toplevel.begin_local_theory true (Instance.instantiation_cmd arities))); 

24589  442 

25485  443 
val _ = 
444 
OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal 

445 
((P.xname  ((P.$$$ "\\<subseteq>"  P.$$$ "<")  P.!!! P.xname) >> Class.classrel_cmd  

25536  446 
P.arity  Scan.repeat (SpecParse.opt_thm_name ":"  P.prop) 
447 
>> (fn (arity, defs) => Instance.instance_cmd arity defs)) 

25485  448 
>> (Toplevel.print oo Toplevel.theory_to_proof) 
449 
 Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I))); 

22299  450 

451 

25519  452 
(* arbitrary overloading *) 
453 

454 
val _ = 

455 
OuterSyntax.command "overloading" "overloaded definitions" K.thy_decl 

25861  456 
(Scan.repeat1 (P.name  (P.$$$ "\\<equiv>"  P.$$$ "==")  P.term  
26048  457 
Scan.optional (P.$$$ "("  (P.$$$ "unchecked" >> K false)  P.$$$ ")") true 
458 
>> P.triple1)  P.begin 

25519  459 
>> (fn operations => Toplevel.print o 
460 
Toplevel.begin_local_theory true (TheoryTarget.overloading_cmd operations))); 

461 

462 

22866  463 
(* code generation *) 
464 

24868  465 
val _ = 
22866  466 
OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl 
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24314
diff
changeset

467 
(Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd)); 
22866  468 

469 

5832  470 

471 
(** proof commands **) 

472 

473 
(* statements *) 

474 

17353  475 
fun gen_theorem kind = 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

476 
OuterSyntax.local_theory_to_proof' kind ("state " ^ kind) K.thy_goal 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

477 
(Scan.optional (SpecParse.opt_thm_name ":"  
22117  478 
Scan.ahead (SpecParse.locale_keyword  SpecParse.statement_keyword)) ("", [])  
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

479 
SpecParse.general_statement >> (fn (a, (elems, concl)) => 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

480 
(Specification.theorem_cmd kind NONE (K I) a elems concl))); 
5832  481 

24868  482 
val _ = gen_theorem Thm.theoremK; 
483 
val _ = gen_theorem Thm.lemmaK; 

484 
val _ = gen_theorem Thm.corollaryK; 

5832  485 

24868  486 
val _ = 
17353  487 
OuterSyntax.command "have" "state local goal" 
488 
(K.tag_proof K.prf_goal) 

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

24868  491 
val _ = 
17353  492 
OuterSyntax.command "hence" "abbreviates \"then have\"" 
493 
(K.tag_proof K.prf_goal) 

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

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

498 
(K.tag_proof K.prf_asm_goal) 
22117  499 
(SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show)); 
5832  500 

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

503 
(K.tag_proof K.prf_asm_goal) 
22117  504 
(SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus)); 
6501  505 

5832  506 

5914  507 
(* facts *) 
5832  508 

22117  509 
val facts = P.and_list1 SpecParse.xthms1; 
9197  510 

24868  511 
val _ = 
17068  512 
OuterSyntax.command "then" "forward chaining" 
513 
(K.tag_proof K.prf_chain) 

17900  514 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain)); 
5832  515 

24868  516 
val _ = 
17068  517 
OuterSyntax.command "from" "forward chaining from given facts" 
518 
(K.tag_proof K.prf_chain) 

17900  519 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss))); 
5914  520 

24868  521 
val _ = 
17068  522 
OuterSyntax.command "with" "forward chaining from given and current facts" 
523 
(K.tag_proof K.prf_chain) 

17900  524 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss))); 
6878  525 

24868  526 
val _ = 
17068  527 
OuterSyntax.command "note" "define facts" 
528 
(K.tag_proof K.prf_decl) 

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

24868  531 
val _ = 
17068  532 
OuterSyntax.command "using" "augment goal facts" 
533 
(K.tag_proof K.prf_decl) 

18544  534 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.using))); 
535 

24868  536 
val _ = 
18544  537 
OuterSyntax.command "unfolding" "unfold definitions in goal and facts" 
538 
(K.tag_proof K.prf_decl) 

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

12926  540 

5832  541 

542 
(* proof context *) 

543 

24868  544 
val _ = 
17068  545 
OuterSyntax.command "fix" "fix local variables (Skolem constants)" 
546 
(K.tag_proof K.prf_asm) 

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

24868  549 
val _ = 
17068  550 
OuterSyntax.command "assume" "assume propositions" 
551 
(K.tag_proof K.prf_asm) 

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

24868  554 
val _ = 
17068  555 
OuterSyntax.command "presume" "assume propositions, to be established later" 
556 
(K.tag_proof K.prf_asm) 

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

24868  559 
val _ = 
17068  560 
OuterSyntax.command "def" "local definition" 
561 
(K.tag_proof K.prf_asm) 

18308  562 
(P.and_list1 
22117  563 
(SpecParse.opt_thm_name ":"  
19844  564 
((P.name  P.opt_mixfix)  ((P.$$$ "\\<equiv>"  P.$$$ "==")  P.!!! P.termp))) 
18308  565 
>> (Toplevel.print oo (Toplevel.proof o Proof.def))); 
6953  566 

24868  567 
val _ = 
11890  568 
OuterSyntax.command "obtain" "generalized existence" 
17068  569 
(K.tag_proof K.prf_asm_goal) 
22117  570 
(P.parname  Scan.optional (P.fixes  P.where_) []  SpecParse.statement 
18895  571 
>> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain x y z))); 
5832  572 

24868  573 
val _ = 
17854  574 
OuterSyntax.command "guess" "wild guessing (unstructured)" 
575 
(K.tag_proof K.prf_asm_goal) 

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

24868  578 
val _ = 
17068  579 
OuterSyntax.command "let" "bind text variables" 
580 
(K.tag_proof K.prf_decl) 

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

581 
(P.and_list1 (P.enum1 "and" P.term  (P.$$$ "="  P.term)) 
17900  582 
>> (Toplevel.print oo (Toplevel.proof o Proof.let_bind))); 
5832  583 

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

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

587 

24868  588 
val _ = 
17068  589 
OuterSyntax.command "case" "invoke local context" 
590 
(K.tag_proof K.prf_asm) 

17900  591 
(case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case))); 
8370  592 

5832  593 

594 
(* proof structure *) 

595 

24868  596 
val _ = 
17068  597 
OuterSyntax.command "{" "begin explicit proof block" 
598 
(K.tag_proof K.prf_open) 

17900  599 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block)); 
5832  600 

24868  601 
val _ = 
17068  602 
OuterSyntax.command "}" "end explicit proof block" 
603 
(K.tag_proof K.prf_close) 

20305  604 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block)); 
6687  605 

24868  606 
val _ = 
17068  607 
OuterSyntax.command "next" "enter next proof block" 
608 
(K.tag_proof K.prf_block) 

17900  609 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block)); 
5832  610 

611 

612 
(* end proof *) 

613 

24868  614 
val _ = 
17068  615 
OuterSyntax.command "qed" "conclude (sub)proof" 
616 
(K.tag_proof K.qed_block) 

26676  617 
(Scan.option Method.parse >> IsarCmd.qed); 
5832  618 

24868  619 
val _ = 
17068  620 
OuterSyntax.command "by" "terminal backward proof" 
621 
(K.tag_proof K.qed) 

26676  622 
(Method.parse  Scan.option Method.parse >> IsarCmd.terminal_proof); 
6404  623 

24868  624 
val _ = 
17068  625 
OuterSyntax.command ".." "default proof" 
626 
(K.tag_proof K.qed) 

26676  627 
(Scan.succeed IsarCmd.default_proof); 
8966  628 

24868  629 
val _ = 
17068  630 
OuterSyntax.command "." "immediate proof" 
631 
(K.tag_proof K.qed) 

26676  632 
(Scan.succeed IsarCmd.immediate_proof); 
6404  633 

24868  634 
val _ = 
17068  635 
OuterSyntax.command "done" "done proof" 
636 
(K.tag_proof K.qed) 

26676  637 
(Scan.succeed IsarCmd.done_proof); 
5832  638 

24868  639 
val _ = 
25108  640 
OuterSyntax.command "sorry" "skip proof (quickanddirty mode only!)" 
17068  641 
(K.tag_proof K.qed) 
26676  642 
(Scan.succeed IsarCmd.skip_proof); 
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
6886
diff
changeset

643 

24868  644 
val _ = 
17068  645 
OuterSyntax.command "oops" "forget proof" 
646 
(K.tag_proof K.qed_global) 

18561  647 
(Scan.succeed Toplevel.forget_proof); 
8210  648 

5832  649 

650 
(* proof steps *) 

651 

24868  652 
val _ = 
17068  653 
OuterSyntax.command "defer" "shuffle internal proof state" 
654 
(K.tag_proof K.prf_script) 

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

24868  657 
val _ = 
17068  658 
OuterSyntax.command "prefer" "shuffle internal proof state" 
659 
(K.tag_proof K.prf_script) 

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

24868  662 
val _ = 
17068  663 
OuterSyntax.command "apply" "initial refinement step (unstructured)" 
664 
(K.tag_proof K.prf_script) 

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

24868  667 
val _ = 
17068  668 
OuterSyntax.command "apply_end" "terminal refinement (unstructured)" 
669 
(K.tag_proof K.prf_script) 

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

24868  672 
val _ = 
17068  673 
OuterSyntax.command "proof" "backward proof" 
674 
(K.tag_proof K.prf_block) 

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

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

677 
Toplevel.skip_proof (History.apply (fn i => i + 1)))); 
5832  678 

679 

6773  680 
(* calculational proof commands *) 
681 

6878  682 
val calc_args = 
22117  683 
Scan.option (P.$$$ "("  P.!!! ((SpecParse.xthms1  P.$$$ ")"))); 
6878  684 

24868  685 
val _ = 
17068  686 
OuterSyntax.command "also" "combine calculation and current facts" 
687 
(K.tag_proof K.prf_decl) 

17900  688 
(calc_args >> (Toplevel.proofs' o Calculation.also)); 
6773  689 

24868  690 
val _ = 
17068  691 
OuterSyntax.command "finally" "combine calculation and current facts, exhibit result" 
692 
(K.tag_proof K.prf_chain) 

22573  693 
(calc_args >> (Toplevel.proofs' o Calculation.finally_)); 
6773  694 

24868  695 
val _ = 
17068  696 
OuterSyntax.command "moreover" "augment calculation by current facts" 
697 
(K.tag_proof K.prf_decl) 

17900  698 
(Scan.succeed (Toplevel.proof' Calculation.moreover)); 
8562  699 

24868  700 
val _ = 
8588  701 
OuterSyntax.command "ultimately" "augment calculation by current facts, exhibit result" 
17068  702 
(K.tag_proof K.prf_chain) 
17900  703 
(Scan.succeed (Toplevel.proof' Calculation.ultimately)); 
8588  704 

6773  705 

6742  706 
(* proof navigation *) 
5944  707 

24868  708 
val _ = 
17068  709 
OuterSyntax.command "back" "backtracking of proof command" 
710 
(K.tag_proof K.prf_script) 

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

5832  712 

713 

6742  714 
(* history *) 
715 

24868  716 
val _ = 
20979  717 
OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control 
718 
(P.name >> (Toplevel.no_timing oo IsarCmd.cannot_undo)); 

6742  719 

24868  720 
val _ = 
6742  721 
OuterSyntax.improper_command "redo" "redo last command" K.control 
9010  722 
(Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.redo)); 
6742  723 

24868  724 
val _ = 
6742  725 
OuterSyntax.improper_command "undos_proof" "undo last proof commands" K.control 
9010  726 
(P.nat >> ((Toplevel.no_timing o Toplevel.print) oo IsarCmd.undos_proof)); 
6742  727 

24868  728 
val _ = 
6742  729 
OuterSyntax.improper_command "undo" "undo last command" K.control 
25192
b568f8c5d5ca
made command 'undo' silent ('ProofGeneral.undo' becomes a historical relic);
wenzelm
parents:
25108
diff
changeset

730 
(Scan.succeed (Toplevel.no_timing o IsarCmd.undo)); 
6742  731 

24868  732 
val _ = 
8500  733 
OuterSyntax.improper_command "kill" "kill current history node" K.control 
22866  734 
(Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.kill)); 
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22573
diff
changeset

735 

5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22573
diff
changeset

736 

25578  737 
(* nested command *) 
738 

739 
val _ = 

740 
OuterSyntax.improper_command "Isabelle.command" "nested Isabelle command" K.control 

25794
11bec58fc289
Isabelle.command: IsarCmd.nested_command (with properties);
wenzelm
parents:
25625
diff
changeset

741 
((Scan.optional P.properties []  P.position P.string) : (fn (props, arg) => 
11bec58fc289
Isabelle.command: IsarCmd.nested_command (with properties);
wenzelm
parents:
25625
diff
changeset

742 
Scan.succeed (K (IsarCmd.nested_command props arg)) 
11bec58fc289
Isabelle.command: IsarCmd.nested_command (with properties);
wenzelm
parents:
25625
diff
changeset

743 
handle ERROR msg => Scan.fail_with (K msg))); 
25578  744 

745 

22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22573
diff
changeset

746 

5832  747 
(** diagnostic commands (for interactive mode only) **) 
748 

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

24868  752 
val _ = 
7124  753 
OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing" 
9010  754 
K.diag (P.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin)); 
7124  755 

24868  756 
val _ = 
21714  757 
OuterSyntax.improper_command "help" "print outer syntax commands" K.diag 
24871  758 
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative OuterSyntax.print_outer_syntax)); 
21714  759 

24868  760 
val _ = 
21714  761 
OuterSyntax.improper_command "print_commands" "print outer syntax commands" K.diag 
24871  762 
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative OuterSyntax.print_outer_syntax)); 
5832  763 

24868  764 
val _ = 
24115  765 
OuterSyntax.improper_command "print_configs" "print configuration options" K.diag 
766 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_configs)); 

23989  767 

24868  768 
val _ = 
7308  769 
OuterSyntax.improper_command "print_context" "print theory context name" K.diag 
9010  770 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_context)); 
7308  771 

24868  772 
val _ = 
6723  773 
OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag 
20621  774 
(opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory)); 
5832  775 

24868  776 
val _ = 
21726  777 
OuterSyntax.improper_command "print_syntax" "print inner syntax of context (verbose!)" K.diag 
9010  778 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax)); 
5832  779 

24868  780 
val _ = 
21726  781 
OuterSyntax.improper_command "print_abbrevs" "print constant abbreviation of context" K.diag 
782 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_abbrevs)); 

783 

24868  784 
val _ = 
17068  785 
OuterSyntax.improper_command "print_theorems" 
786 
"print theorems of local theory or proof context" K.diag 

9010  787 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_theorems)); 
5881  788 

24868  789 
val _ = 
12061  790 
OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag 
791 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_locales)); 

792 

24868  793 
val _ = 
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22573
diff
changeset

794 
OuterSyntax.improper_command "print_classes" "print classes of this theory" K.diag 
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22573
diff
changeset

795 
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory 
24219  796 
o Toplevel.keep (Class.print_classes o Toplevel.theory_of))); 
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22573
diff
changeset

797 

24868  798 
val _ = 
15596  799 
OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag 
20621  800 
(opt_bang  locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale)); 
12061  801 

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

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

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

15596  807 

24868  808 
val _ = 
12061  809 
OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag 
9010  810 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes)); 
5832  811 

24868  812 
val _ = 
16027  813 
OuterSyntax.improper_command "print_simpset" "print context of Simplifier" K.diag 
814 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_simpset)); 

815 

24868  816 
val _ = 
12383  817 
OuterSyntax.improper_command "print_rules" "print intro/elim rules" K.diag 
818 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_rules)); 

819 

24868  820 
val _ = 
11666  821 
OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" K.diag 
9221  822 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules)); 
823 

24868  824 
val _ = 
12061  825 
OuterSyntax.improper_command "print_methods" "print methods of this theory" K.diag 
9010  826 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods)); 
5832  827 

24868  828 
val _ = 
9221  829 
OuterSyntax.improper_command "print_antiquotations" "print antiquotations (global)" K.diag 
830 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations)); 

831 

24868  832 
val _ = 
22485  833 
OuterSyntax.improper_command "thy_deps" "visualize theory dependencies" 
834 
K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.thy_deps)); 

835 

24868  836 
val _ = 
20574  837 
OuterSyntax.improper_command "class_deps" "visualize class dependencies" 
838 
K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps)); 

839 

24868  840 
val _ = 
9454  841 
OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies" 
22117  842 
K.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps)); 
9454  843 

22866  844 
local 
845 

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

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

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

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

16074  851 
P.reserved "simp"  P.!!! (P.$$$ ":"  P.term) >> FindTheorems.Simp  
16027  852 
P.term >> FindTheorems.Pattern; 
853 

22866  854 
val options = 
855 
Scan.optional 

856 
(P.$$$ "("  

857 
P.!!! (Scan.option P.nat  Scan.optional (P.reserved "with_dups" >> K false) true 

858 
 P.$$$ ")")) (NONE, true); 

859 
in 

860 

24868  861 
val _ = 
22866  862 
OuterSyntax.improper_command "find_theorems" "print theorems meeting specified criteria" K.diag 
863 
(options  Scan.repeat (((Scan.option P.minus >> is_none)  criterion)) 

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

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

865 

22866  866 
end; 
867 

24868  868 
val _ = 
6723  869 
OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag 
9010  870 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds)); 
5832  871 

24868  872 
val _ = 
8370  873 
OuterSyntax.improper_command "print_facts" "print facts of proof context" K.diag 
21004  874 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_facts)); 
5832  875 

24868  876 
val _ = 
8370  877 
OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag 
9010  878 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases)); 
8370  879 

24868  880 
val _ = 
19269  881 
OuterSyntax.improper_command "print_statement" "print theorems as long statements" K.diag 
22117  882 
(opt_modes  SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts)); 
19269  883 

24868  884 
val _ = 
8464  885 
OuterSyntax.improper_command "thm" "print theorems" K.diag 
22117  886 
(opt_modes  SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms)); 
5832  887 

24868  888 
val _ = 
11524
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11101
diff
changeset

889 
OuterSyntax.improper_command "prf" "print proof terms of theorems" K.diag 
22866  890 
(opt_modes  Scan.option SpecParse.xthms1 
891 
>> (Toplevel.no_timing oo IsarCmd.print_prfs false)); 

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

892 

24868  893 
val _ = 
11524
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11101
diff
changeset

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

896 

24868  897 
val _ = 
6723  898 
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

899 
(opt_modes  P.term >> (Toplevel.no_timing oo IsarCmd.print_prop)); 
5832  900 

24868  901 
val _ = 
6723  902 
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

903 
(opt_modes  P.term >> (Toplevel.no_timing oo IsarCmd.print_term)); 
5832  904 

24868  905 
val _ = 
6723  906 
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

907 
(opt_modes  P.typ >> (Toplevel.no_timing oo IsarCmd.print_type)); 
5832  908 

24868  909 
val _ = 
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22573
diff
changeset

910 
OuterSyntax.improper_command "print_codesetup" "print code generator setup of this theory" K.diag 
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22573
diff
changeset

911 
(Scan.succeed 
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22573
diff
changeset

912 
(Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep 
24219  913 
(Code.print_codesetup o Toplevel.theory_of))); 
5832  914 

26184  915 
val _ = 
916 
OuterSyntax.improper_command "unused_thms" "find unused theorems" K.diag 

917 
(Scan.option ((Scan.repeat1 (Scan.unless P.minus P.name)  P.minus)  

918 
Scan.option (Scan.repeat1 (Scan.unless P.minus P.name))) >> 

919 
(Toplevel.no_timing oo IsarCmd.unused_thms)); 

920 

5832  921 

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

923 

24868  924 
val _ = 
8650  925 
OuterSyntax.improper_command "cd" "change current working directory" K.diag 
14950  926 
(P.path >> (Toplevel.no_timing oo IsarCmd.cd)); 
5832  927 

24868  928 
val _ = 
6723  929 
OuterSyntax.improper_command "pwd" "print current working directory" K.diag 
9010  930 
(Scan.succeed (Toplevel.no_timing o IsarCmd.pwd)); 
5832  931 

24868  932 
val _ = 
6723  933 
OuterSyntax.improper_command "use_thy" "use theory file" K.diag 
26404  934 
(P.name >> (fn name => 
935 
Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.use_thy name))); 

5832  936 

24868  937 
val _ = 
7102  938 
OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag 
9010  939 
(P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy)); 
7102  940 

24868  941 
val _ = 
7908  942 
OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag 
9010  943 
(P.name >> (Toplevel.no_timing oo IsarCmd.touch_child_thys)); 
7908  944 

24868  945 
val _ = 
7102  946 
OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag 
9010  947 
(P.name >> (Toplevel.no_timing oo IsarCmd.remove_thy)); 
7102  948 

24868  949 
val _ = 
7931  950 
OuterSyntax.improper_command "kill_thy" "kill theory  try to remove from loader database" 
9010  951 
K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.kill_thy)); 
7931  952 

24868  953 
val _ = 
14934  954 
OuterSyntax.improper_command "display_drafts" "display raw source files with symbols" 
14950  955 
K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.display_drafts)); 
14934  956 

24868  957 
val _ = 
14934  958 
OuterSyntax.improper_command "print_drafts" "print raw source files with symbols" 
14950  959 
K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.print_drafts)); 
14934  960 

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

963 

24868  964 
val _ = 
8886  965 
OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag 
9731  966 
(opt_modes  opt_limits >> (Toplevel.no_timing oo IsarCmd.pr)); 
7199  967 

24868  968 
val _ = 
7222  969 
OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" K.diag 
9010  970 
(Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr)); 
5832  971 

24868  972 
val _ = 
7222  973 
OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag 
9010  974 
(Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr)); 
7222  975 

24868  976 
val _ = 
6723  977 
OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag 
26490  978 
(P.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit)); 
5832  979 

24868  980 
val _ = 
6723  981 
OuterSyntax.improper_command "quit" "quit Isabelle" K.control 
9010  982 
(P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit)); 
5832  983 

24868  984 
val _ = 
6723  985 
OuterSyntax.improper_command "exit" "exit Isar loop" K.control 
9010  986 
(Scan.succeed (Toplevel.no_timing o IsarCmd.exit)); 
5832  987 

24868  988 
val _ = 
7102  989 
OuterSyntax.improper_command "init_toplevel" "restart Isar toplevel loop" K.control 
9010  990 
(Scan.succeed (Toplevel.no_timing o IsarCmd.init_toplevel)); 
5991  991 

24868  992 
val _ = 
8678  993 
OuterSyntax.improper_command "welcome" "print welcome message" K.diag 
9010  994 
(Scan.succeed (Toplevel.no_timing o IsarCmd.welcome)); 
7462  995 

5832  996 
end; 