author  wenzelm 
Fri, 07 Dec 2007 22:19:49 +0100  
changeset 25578  11ee8b183477 
parent 25536  01753a944433 
child 25585  19cd3474fdf3 
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>", "]", 

23 
"advanced", "and", "assumes", "attach", "begin", "binder", "concl", 

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 _ = 
19076  235 
OuterSyntax.command "definition" "constant definition" K.thy_decl 
22117  236 
(P.opt_target  constdef 
24932
86ef9a828a9e
AxClass.axiomatize and Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
wenzelm
parents:
24914
diff
changeset

237 
>> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.definition_cmd args))); 
18780  238 

24868  239 
val _ = 
19076  240 
OuterSyntax.command "abbreviation" "constant abbreviation" K.thy_decl 
22117  241 
(P.opt_target  opt_mode  (Scan.option constdecl  P.prop) 
19659  242 
>> (fn ((loc, mode), args) => 
24932
86ef9a828a9e
AxClass.axiomatize and Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
wenzelm
parents:
24914
diff
changeset

243 
Toplevel.local_theory loc (Specification.abbreviation_cmd mode args))); 
19659  244 

24868  245 
val _ = 
24950  246 
OuterSyntax.command "notation" "add notation for constants / fixed variables" K.thy_decl 
24953  247 
(P.opt_target  opt_mode  P.and_list1 (P.xname  SpecParse.locale_mixfix) 
19659  248 
>> (fn ((loc, mode), args) => 
24950  249 
Toplevel.local_theory loc (Specification.notation_cmd true mode args))); 
250 

251 
val _ = 

252 
OuterSyntax.command "no_notation" "delete notation for constants / fixed variables" K.thy_decl 

24953  253 
(P.opt_target  opt_mode  P.and_list1 (P.xname  SpecParse.locale_mixfix) 
24950  254 
>> (fn ((loc, mode), args) => 
255 
Toplevel.local_theory loc (Specification.notation_cmd false mode args))); 

19076  256 

5832  257 

18616  258 
(* constant specifications *) 
259 

24868  260 
val _ = 
18616  261 
OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl 
22117  262 
(P.opt_target  
18949  263 
(Scan.optional P.fixes []  
22117  264 
Scan.optional (P.where_  P.!!! (P.and_list1 SpecParse.spec)) []) 
24932
86ef9a828a9e
AxClass.axiomatize and Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
wenzelm
parents:
24914
diff
changeset

265 
>> (fn (loc, (x, y)) => Toplevel.local_theory loc (#2 o Specification.axiomatization_cmd x y))); 
18616  266 

267 

5914  268 
(* theorems *) 
269 

22117  270 
fun theorems kind = P.opt_target  SpecParse.name_facts 
24932
86ef9a828a9e
AxClass.axiomatize and Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
wenzelm
parents:
24914
diff
changeset

271 
>> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.theorems_cmd kind args)); 
12712  272 

24868  273 
val _ = 
21437  274 
OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK); 
5914  275 

24868  276 
val _ = 
21437  277 
OuterSyntax.command "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK); 
5914  278 

24868  279 
val _ = 
23795  280 
OuterSyntax.command "declare" "declare theorems (improper)" K.thy_decl 
22117  281 
(P.opt_target  (P.and_list1 SpecParse.xthms1 >> flat) 
20907  282 
>> (fn (loc, args) => Toplevel.local_theory loc 
24932
86ef9a828a9e
AxClass.axiomatize and Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
wenzelm
parents:
24914
diff
changeset

283 
(#2 o Specification.theorems_cmd "" [(("", []), args)]))); 
9589  284 

5914  285 

5832  286 
(* name space entry path *) 
287 

24868  288 
val _ = 
6723  289 
OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl 
16447  290 
(Scan.succeed (Toplevel.theory Sign.root_path)); 
5832  291 

24868  292 
val _ = 
6723  293 
OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl 
16447  294 
(Scan.succeed (Toplevel.theory Sign.local_path)); 
8723  295 

24868  296 
val _ = 
8723  297 
OuterSyntax.command "hide" "hide names from given name space" K.thy_decl 
17397  298 
((P.opt_keyword "open" >> not)  (P.name  Scan.repeat1 P.xname) >> 
299 
(Toplevel.theory o uncurry Sign.hide_names)); 

5832  300 

301 

302 
(* use ML text *) 

303 

24868  304 
val _ = 
17068  305 
OuterSyntax.command "use" "eval ML text from file" (K.tag_ml K.diag) 
14950  306 
(P.path >> (Toplevel.no_timing oo IsarCmd.use)); 
5832  307 

24868  308 
val _ = 
17068  309 
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

310 
(P.text >> IsarCmd.use_mltext true); 
7891  311 

24868  312 
val _ = 
17068  313 
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

314 
(P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false)); 
7616  315 

24868  316 
val _ = 
17068  317 
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

318 
(P.text >> IsarCmd.use_mltext_theory); 
5832  319 

24868  320 
val _ = 
17068  321 
OuterSyntax.command "setup" "apply ML theory setup" (K.tag_ml K.thy_decl) 
22117  322 
(Scan.option P.text >> (Toplevel.theory o IsarCmd.generic_setup)); 
5832  323 

24868  324 
val _ = 
17068  325 
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

326 
(((P.name  P.!!! (P.$$$ "="  P.text  P.text) >> P.triple2)) 
17353  327 
>> (Toplevel.theory o Method.method_setup)); 
9197  328 

24868  329 
val _ = 
22088  330 
OuterSyntax.command "declaration" "generic ML declaration" (K.tag_ml K.thy_decl) 
22117  331 
(P.opt_target  P.text 
22088  332 
>> (fn (loc, txt) => Toplevel.local_theory loc (IsarCmd.declaration txt))); 
333 

24868  334 
val _ = 
22202  335 
OuterSyntax.command "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl) 
336 
(P.opt_target  

22239  337 
P.name  (P.$$$ "("  P.enum1 "" P.term  P.$$$ ")"  P.$$$ "=")  P.text  
338 
Scan.optional (P.$$$ "identifier"  Scan.repeat1 P.xname) [] 

339 
>> (fn ((((loc, a), b), c), d) => Toplevel.local_theory loc (IsarCmd.simproc_setup a b c d))); 

22202  340 

5832  341 

342 
(* translation functions *) 

343 

14642  344 
val trfun = P.opt_keyword "advanced"  P.text; 
345 

24868  346 
val _ = 
17068  347 
OuterSyntax.command "parse_ast_translation" "install parse ast translation functions" 
348 
(K.tag_ml K.thy_decl) 

22117  349 
(trfun >> (Toplevel.theory o IsarCmd.parse_ast_translation)); 
5832  350 

24868  351 
val _ = 
17068  352 
OuterSyntax.command "parse_translation" "install parse translation functions" 
353 
(K.tag_ml K.thy_decl) 

22117  354 
(trfun >> (Toplevel.theory o IsarCmd.parse_translation)); 
5832  355 

24868  356 
val _ = 
17068  357 
OuterSyntax.command "print_translation" "install print translation functions" 
358 
(K.tag_ml K.thy_decl) 

22117  359 
(trfun >> (Toplevel.theory o IsarCmd.print_translation)); 
5832  360 

24868  361 
val _ = 
6370  362 
OuterSyntax.command "typed_print_translation" "install typed print translation functions" 
17068  363 
(K.tag_ml K.thy_decl) 
22117  364 
(trfun >> (Toplevel.theory o IsarCmd.typed_print_translation)); 
5832  365 

24868  366 
val _ = 
17068  367 
OuterSyntax.command "print_ast_translation" "install print ast translation functions" 
368 
(K.tag_ml K.thy_decl) 

22117  369 
(trfun >> (Toplevel.theory o IsarCmd.print_ast_translation)); 
5832  370 

24868  371 
val _ = 
17068  372 
OuterSyntax.command "token_translation" "install token translation functions" 
373 
(K.tag_ml K.thy_decl) 

22117  374 
(P.text >> (Toplevel.theory o IsarCmd.token_translation)); 
5832  375 

376 

377 
(* oracles *) 

378 

24868  379 
val _ = 
17068  380 
OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl) 
16849  381 
(P.name  (P.$$$ "("  P.text  P.$$$ ")"  P.$$$ "=") 
22239  382 
 P.text >> (fn ((x, y), z) => Toplevel.theory (IsarCmd.oracle x y z))); 
5832  383 

384 

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

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

386 

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

388 
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

389 
(P.name  P.begin >> (fn name => 
25290  390 
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

391 

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

392 

12061  393 
(* locales *) 
394 

12758  395 
val locale_val = 
24868  396 
SpecParse.locale_expr  
22117  397 
Scan.optional (P.$$$ "+"  P.!!! (Scan.repeat1 SpecParse.context_element)) []  
24868  398 
Scan.repeat1 SpecParse.context_element >> pair Locale.empty; 
12061  399 

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

20958  404 
>> (fn (((is_open, name), (expr, elems)), begin) => 
21843  405 
(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

406 
(Locale.add_locale is_open name expr elems #> TheoryTarget.begin))); 
12061  407 

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

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

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

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

12061  416 

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

418 
OuterSyntax.command "interpret" 
17068  419 
"prove and register interpretation of locale expression in proof context" 
420 
(K.tag_proof K.prf_goal) 

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

15703  424 

425 

22299  426 
(* classes *) 
427 

24868  428 
val class_val = 
429 
SpecParse.class_expr  

430 
Scan.optional (P.$$$ "+"  P.!!! (Scan.repeat1 SpecParse.locale_element)) []  

431 
Scan.repeat1 SpecParse.locale_element >> pair []; 

22299  432 

24868  433 
val _ = 
434 
OuterSyntax.command "class" "define type class" K.thy_decl 

435 
(P.name  

436 
Scan.optional (P.$$$ "("  P.$$$ "attach"  Scan.repeat P.term  P.$$$ ")") []  (* FIXME ?? *) 

437 
(P.$$$ "="  class_val)  P.opt_begin 

25003  438 
>> (fn (((name, add_consts), (supclasses, elems)), begin) => 
24938  439 
(begin ? Toplevel.print) o Toplevel.begin_local_theory begin 
25003  440 
(Class.class_cmd name supclasses elems add_consts #> TheoryTarget.begin))); 
22299  441 

24868  442 
val _ = 
24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24871
diff
changeset

443 
OuterSyntax.command "subclass" "prove a subclass relation" K.thy_goal 
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24871
diff
changeset

444 
(P.opt_target  P.xname >> (fn (loc, class) => 
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24871
diff
changeset

445 
Toplevel.print o Toplevel.local_theory_to_proof loc (Subclass.subclass_cmd class))); 
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24871
diff
changeset

446 

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

447 
val _ = 
25519  448 
OuterSyntax.command "instantiation" "instantiate and prove type arity" K.thy_decl 
25536  449 
(P.multi_arity  P.begin 
25462  450 
>> (fn arities => Toplevel.print o 
451 
Toplevel.begin_local_theory true (Instance.instantiation_cmd arities))); 

24589  452 

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

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

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

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

22299  460 

461 

25519  462 
(* arbitrary overloading *) 
463 

464 
val _ = 

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

466 
(Scan.repeat1 (P.xname  P.$$$ "::"  P.typ  P.$$$ "is"  P.name  

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

468 
 P.begin 

469 
>> (fn operations => Toplevel.print o 

470 
Toplevel.begin_local_theory true (TheoryTarget.overloading_cmd operations))); 

471 

472 

22866  473 
(* code generation *) 
474 

24868  475 
val _ = 
22866  476 
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

477 
(Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd)); 
22866  478 

479 

5832  480 

481 
(** proof commands **) 

482 

483 
(* statements *) 

484 

17353  485 
fun gen_theorem kind = 
486 
OuterSyntax.command kind ("state " ^ kind) K.thy_goal 

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

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

21033  490 
(Toplevel.print o 
24451
7c205d006719
Specification.theorem now also takes "interactive" flag as argument.
berghofe
parents:
24423
diff
changeset

491 
Toplevel.local_theory_to_proof' loc 
24932
86ef9a828a9e
AxClass.axiomatize and Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
wenzelm
parents:
24914
diff
changeset

492 
(Specification.theorem_cmd kind NONE (K I) a elems concl)))); 
5832  493 

24868  494 
val _ = gen_theorem Thm.theoremK; 
495 
val _ = gen_theorem Thm.lemmaK; 

496 
val _ = gen_theorem Thm.corollaryK; 

5832  497 

24868  498 
val _ = 
17353  499 
OuterSyntax.command "have" "state local goal" 
500 
(K.tag_proof K.prf_goal) 

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

24868  503 
val _ = 
17353  504 
OuterSyntax.command "hence" "abbreviates \"then have\"" 
505 
(K.tag_proof K.prf_goal) 

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

24868  508 
val _ = 
17068  509 
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

510 
(K.tag_proof K.prf_asm_goal) 
22117  511 
(SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show)); 
5832  512 

24868  513 
val _ = 
17068  514 
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

515 
(K.tag_proof K.prf_asm_goal) 
22117  516 
(SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus)); 
6501  517 

5832  518 

5914  519 
(* facts *) 
5832  520 

22117  521 
val facts = P.and_list1 SpecParse.xthms1; 
9197  522 

24868  523 
val _ = 
17068  524 
OuterSyntax.command "then" "forward chaining" 
525 
(K.tag_proof K.prf_chain) 

17900  526 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain)); 
5832  527 

24868  528 
val _ = 
17068  529 
OuterSyntax.command "from" "forward chaining from given facts" 
530 
(K.tag_proof K.prf_chain) 

17900  531 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss))); 
5914  532 

24868  533 
val _ = 
17068  534 
OuterSyntax.command "with" "forward chaining from given and current facts" 
535 
(K.tag_proof K.prf_chain) 

17900  536 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss))); 
6878  537 

24868  538 
val _ = 
17068  539 
OuterSyntax.command "note" "define facts" 
540 
(K.tag_proof K.prf_decl) 

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

24868  543 
val _ = 
17068  544 
OuterSyntax.command "using" "augment goal facts" 
545 
(K.tag_proof K.prf_decl) 

18544  546 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.using))); 
547 

24868  548 
val _ = 
18544  549 
OuterSyntax.command "unfolding" "unfold definitions in goal and facts" 
550 
(K.tag_proof K.prf_decl) 

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

12926  552 

5832  553 

554 
(* proof context *) 

555 

24868  556 
val _ = 
17068  557 
OuterSyntax.command "fix" "fix local variables (Skolem constants)" 
558 
(K.tag_proof K.prf_asm) 

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

24868  561 
val _ = 
17068  562 
OuterSyntax.command "assume" "assume propositions" 
563 
(K.tag_proof K.prf_asm) 

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

24868  566 
val _ = 
17068  567 
OuterSyntax.command "presume" "assume propositions, to be established later" 
568 
(K.tag_proof K.prf_asm) 

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

24868  571 
val _ = 
17068  572 
OuterSyntax.command "def" "local definition" 
573 
(K.tag_proof K.prf_asm) 

18308  574 
(P.and_list1 
22117  575 
(SpecParse.opt_thm_name ":"  
19844  576 
((P.name  P.opt_mixfix)  ((P.$$$ "\\<equiv>"  P.$$$ "==")  P.!!! P.termp))) 
18308  577 
>> (Toplevel.print oo (Toplevel.proof o Proof.def))); 
6953  578 

24868  579 
val _ = 
11890  580 
OuterSyntax.command "obtain" "generalized existence" 
17068  581 
(K.tag_proof K.prf_asm_goal) 
22117  582 
(P.parname  Scan.optional (P.fixes  P.where_) []  SpecParse.statement 
18895  583 
>> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain x y z))); 
5832  584 

24868  585 
val _ = 
17854  586 
OuterSyntax.command "guess" "wild guessing (unstructured)" 
587 
(K.tag_proof K.prf_asm_goal) 

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

24868  590 
val _ = 
17068  591 
OuterSyntax.command "let" "bind text variables" 
592 
(K.tag_proof K.prf_decl) 

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

593 
(P.and_list1 (P.enum1 "and" P.term  (P.$$$ "="  P.term)) 
17900  594 
>> (Toplevel.print oo (Toplevel.proof o Proof.let_bind))); 
5832  595 

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

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

599 

24868  600 
val _ = 
17068  601 
OuterSyntax.command "case" "invoke local context" 
602 
(K.tag_proof K.prf_asm) 

17900  603 
(case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case))); 
8370  604 

5832  605 

606 
(* proof structure *) 

607 

24868  608 
val _ = 
17068  609 
OuterSyntax.command "{" "begin explicit proof block" 
610 
(K.tag_proof K.prf_open) 

17900  611 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block)); 
5832  612 

24868  613 
val _ = 
17068  614 
OuterSyntax.command "}" "end explicit proof block" 
615 
(K.tag_proof K.prf_close) 

20305  616 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block)); 
6687  617 

24868  618 
val _ = 
17068  619 
OuterSyntax.command "next" "enter next proof block" 
620 
(K.tag_proof K.prf_block) 

17900  621 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block)); 
5832  622 

623 

624 
(* end proof *) 

625 

24868  626 
val _ = 
17068  627 
OuterSyntax.command "qed" "conclude (sub)proof" 
628 
(K.tag_proof K.qed_block) 

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

24868  631 
val _ = 
17068  632 
OuterSyntax.command "by" "terminal backward proof" 
633 
(K.tag_proof K.qed) 

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

24868  636 
val _ = 
17068  637 
OuterSyntax.command ".." "default proof" 
638 
(K.tag_proof K.qed) 

21350  639 
(Scan.succeed (Toplevel.print3 o IsarCmd.default_proof)); 
8966  640 

24868  641 
val _ = 
17068  642 
OuterSyntax.command "." "immediate proof" 
643 
(K.tag_proof K.qed) 

21350  644 
(Scan.succeed (Toplevel.print3 o IsarCmd.immediate_proof)); 
6404  645 

24868  646 
val _ = 
17068  647 
OuterSyntax.command "done" "done proof" 
648 
(K.tag_proof K.qed) 

21350  649 
(Scan.succeed (Toplevel.print3 o IsarCmd.done_proof)); 
5832  650 

24868  651 
val _ = 
25108  652 
OuterSyntax.command "sorry" "skip proof (quickanddirty mode only!)" 
17068  653 
(K.tag_proof K.qed) 
21350  654 
(Scan.succeed (Toplevel.print3 o IsarCmd.skip_proof)); 
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
6886
diff
changeset

655 

24868  656 
val _ = 
17068  657 
OuterSyntax.command "oops" "forget proof" 
658 
(K.tag_proof K.qed_global) 

18561  659 
(Scan.succeed Toplevel.forget_proof); 
8210  660 

5832  661 

662 
(* proof steps *) 

663 

24868  664 
val _ = 
17068  665 
OuterSyntax.command "defer" "shuffle internal proof state" 
666 
(K.tag_proof K.prf_script) 

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

24868  669 
val _ = 
17068  670 
OuterSyntax.command "prefer" "shuffle internal proof state" 
671 
(K.tag_proof K.prf_script) 

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

24868  674 
val _ = 
17068  675 
OuterSyntax.command "apply" "initial refinement step (unstructured)" 
676 
(K.tag_proof K.prf_script) 

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

24868  679 
val _ = 
17068  680 
OuterSyntax.command "apply_end" "terminal refinement (unstructured)" 
681 
(K.tag_proof K.prf_script) 

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

24868  684 
val _ = 
17068  685 
OuterSyntax.command "proof" "backward proof" 
686 
(K.tag_proof K.prf_block) 

22117  687 
(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

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

689 
Toplevel.skip_proof (History.apply (fn i => i + 1)))); 
5832  690 

691 

6773  692 
(* calculational proof commands *) 
693 

6878  694 
val calc_args = 
22117  695 
Scan.option (P.$$$ "("  P.!!! ((SpecParse.xthms1  P.$$$ ")"))); 
6878  696 

24868  697 
val _ = 
17068  698 
OuterSyntax.command "also" "combine calculation and current facts" 
699 
(K.tag_proof K.prf_decl) 

17900  700 
(calc_args >> (Toplevel.proofs' o Calculation.also)); 
6773  701 

24868  702 
val _ = 
17068  703 
OuterSyntax.command "finally" "combine calculation and current facts, exhibit result" 
704 
(K.tag_proof K.prf_chain) 

22573  705 
(calc_args >> (Toplevel.proofs' o Calculation.finally_)); 
6773  706 

24868  707 
val _ = 
17068  708 
OuterSyntax.command "moreover" "augment calculation by current facts" 
709 
(K.tag_proof K.prf_decl) 

17900  710 
(Scan.succeed (Toplevel.proof' Calculation.moreover)); 
8562  711 

24868  712 
val _ = 
8588  713 
OuterSyntax.command "ultimately" "augment calculation by current facts, exhibit result" 
17068  714 
(K.tag_proof K.prf_chain) 
17900  715 
(Scan.succeed (Toplevel.proof' Calculation.ultimately)); 
8588  716 

6773  717 

6742  718 
(* proof navigation *) 
5944  719 

24868  720 
val _ = 
17068  721 
OuterSyntax.command "back" "backtracking of proof command" 
722 
(K.tag_proof K.prf_script) 

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

5832  724 

725 

6742  726 
(* history *) 
727 

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

6742  731 

24868  732 
val _ = 
6742  733 
OuterSyntax.improper_command "redo" "redo last command" K.control 
9010  734 
(Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.redo)); 
6742  735 

24868  736 
val _ = 
6742  737 
OuterSyntax.improper_command "undos_proof" "undo last proof commands" K.control 
9010  738 
(P.nat >> ((Toplevel.no_timing o Toplevel.print) oo IsarCmd.undos_proof)); 
6742  739 

24868  740 
val _ = 
6742  741 
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

742 
(Scan.succeed (Toplevel.no_timing o IsarCmd.undo)); 
6742  743 

24868  744 
val _ = 
8500  745 
OuterSyntax.improper_command "kill" "kill current history node" K.control 
22866  746 
(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

747 

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

748 

25578  749 
(* nested command *) 
750 

751 
val _ = 

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

753 
(P.position P.string : (fn (str, pos) => 

754 
(case OuterSyntax.parse pos str of 

755 
[transition] => Scan.succeed (K transition) 

756 
 _ => Scan.fail_with (K "exactly one nested Isabelle command expected")) 

757 
handle ERROR msg => Scan.fail_with (K ("malformed nested command\n" ^ msg)))); 

758 

759 

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

760 

5832  761 
(** diagnostic commands (for interactive mode only) **) 
762 

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

24868  766 
val _ = 
7124  767 
OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing" 
9010  768 
K.diag (P.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin)); 
7124  769 

24868  770 
val _ = 
21714  771 
OuterSyntax.improper_command "help" "print outer syntax commands" K.diag 
24871  772 
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative OuterSyntax.print_outer_syntax)); 
21714  773 

24868  774 
val _ = 
21714  775 
OuterSyntax.improper_command "print_commands" "print outer syntax commands" K.diag 
24871  776 
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative OuterSyntax.print_outer_syntax)); 
5832  777 

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

23989  781 

24868  782 
val _ = 
7308  783 
OuterSyntax.improper_command "print_context" "print theory context name" K.diag 
9010  784 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_context)); 
7308  785 

24868  786 
val _ = 
6723  787 
OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag 
20621  788 
(opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory)); 
5832  789 

24868  790 
val _ = 
21726  791 
OuterSyntax.improper_command "print_syntax" "print inner syntax of context (verbose!)" K.diag 
9010  792 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax)); 
5832  793 

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

797 

24868  798 
val _ = 
17068  799 
OuterSyntax.improper_command "print_theorems" 
800 
"print theorems of local theory or proof context" K.diag 

9010  801 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_theorems)); 
5881  802 

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

806 

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

808 
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

809 
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory 
24219  810 
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

811 

24868  812 
val _ = 
15596  813 
OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag 
20621  814 
(opt_bang  locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale)); 
12061  815 

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

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

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

15596  821 

24868  822 
val _ = 
12061  823 
OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag 
9010  824 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes)); 
5832  825 

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

829 

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

833 

24868  834 
val _ = 
11666  835 
OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" K.diag 
9221  836 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules)); 
837 

24868  838 
val _ = 
12061  839 
OuterSyntax.improper_command "print_methods" "print methods of this theory" K.diag 
9010  840 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods)); 
5832  841 

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

845 

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

849 

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

853 

24868  854 
val _ = 
9454  855 
OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies" 
22117  856 
K.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps)); 
9454  857 

22866  858 
local 
859 

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

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

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

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

16074  865 
P.reserved "simp"  P.!!! (P.$$$ ":"  P.term) >> FindTheorems.Simp  
16027  866 
P.term >> FindTheorems.Pattern; 
867 

22866  868 
val options = 
869 
Scan.optional 

870 
(P.$$$ "("  

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

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

873 
in 

874 

24868  875 
val _ = 
22866  876 
OuterSyntax.improper_command "find_theorems" "print theorems meeting specified criteria" K.diag 
877 
(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

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

879 

22866  880 
end; 
881 

24868  882 
val _ = 
6723  883 
OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag 
9010  884 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds)); 
5832  885 

24868  886 
val _ = 
8370  887 
OuterSyntax.improper_command "print_facts" "print facts of proof context" K.diag 
21004  888 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_facts)); 
5832  889 

24868  890 
val _ = 
8370  891 
OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag 
9010  892 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases)); 
8370  893 

24868  894 
val _ = 
19269  895 
OuterSyntax.improper_command "print_statement" "print theorems as long statements" K.diag 
22117  896 
(opt_modes  SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts)); 
19269  897 

24868  898 
val _ = 
8464  899 
OuterSyntax.improper_command "thm" "print theorems" K.diag 
22117  900 
(opt_modes  SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms)); 
5832  901 

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

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

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

906 

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

908 
OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" K.diag 
22117  909 
(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

910 

24868  911 
val _ = 
6723  912 
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

913 
(opt_modes  P.term >> (Toplevel.no_timing oo IsarCmd.print_prop)); 
5832  914 

24868  915 
val _ = 
6723  916 
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

917 
(opt_modes  P.term >> (Toplevel.no_timing oo IsarCmd.print_term)); 
5832  918 

24868  919 
val _ = 
6723  920 
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

921 
(opt_modes  P.typ >> (Toplevel.no_timing oo IsarCmd.print_type)); 
5832  922 

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

924 
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

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

926 
(Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep 
24219  927 
(Code.print_codesetup o Toplevel.theory_of))); 
5832  928 

929 

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

931 

24868  932 
val _ = 
8650  933 
OuterSyntax.improper_command "cd" "change current working directory" K.diag 
14950  934 
(P.path >> (Toplevel.no_timing oo IsarCmd.cd)); 
5832  935 

24868  936 
val _ = 
6723  937 
OuterSyntax.improper_command "pwd" "print current working directory" K.diag 
9010  938 
(Scan.succeed (Toplevel.no_timing o IsarCmd.pwd)); 
5832  939 

24868  940 
val _ = 
6723  941 
OuterSyntax.improper_command "use_thy" "use theory file" K.diag 
9010  942 
(P.name >> (Toplevel.no_timing oo IsarCmd.use_thy)); 
5832  943 

24868  944 
val _ = 
7102  945 
OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag 
9010  946 
(P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy)); 
7102  947 

24868  948 
val _ = 
7908  949 
OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag 
9010  950 
(P.name >> (Toplevel.no_timing oo IsarCmd.touch_child_thys)); 
7908  951 

24868  952 
val _ = 
7102  953 
OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag 
9010  954 
(P.name >> (Toplevel.no_timing oo IsarCmd.remove_thy)); 
7102  955 

24868  956 
val _ = 
7931  957 
OuterSyntax.improper_command "kill_thy" "kill theory  try to remove from loader database" 
9010  958 
K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.kill_thy)); 
7931  959 

24868  960 
val _ = 
14934  961 
OuterSyntax.improper_command "display_drafts" "display raw source files with symbols" 
14950  962 
K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.display_drafts)); 
14934  963 

24868  964 
val _ = 
14934  965 
OuterSyntax.improper_command "print_drafts" "print raw source files with symbols" 
14950  966 
K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.print_drafts)); 
14934  967 

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

970 

24868  971 
val _ = 
8886  972 
OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag 
9731  973 
(opt_modes  opt_limits >> (Toplevel.no_timing oo IsarCmd.pr)); 
7199  974 

24868  975 
val _ = 
7222  976 
OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" K.diag 
9010  977 
(Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr)); 
5832  978 

24868  979 
val _ = 
7222  980 
OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag 
9010  981 
(Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr)); 
7222  982 

24868  983 
val _ = 
6723  984 
OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag 
9010  985 
(P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.use_commit)); 
5832  986 

24868  987 
val _ = 
6723  988 
OuterSyntax.improper_command "quit" "quit Isabelle" K.control 
9010  989 
(P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit)); 
5832  990 

24868  991 
val _ = 
6723  992 
OuterSyntax.improper_command "exit" "exit Isar loop" K.control 
9010  993 
(Scan.succeed (Toplevel.no_timing o IsarCmd.exit)); 
5832  994 

24868  995 
val _ = 
7102  996 
OuterSyntax.improper_command "init_toplevel" "restart Isar toplevel loop" K.control 
9010  997 
(Scan.succeed (Toplevel.no_timing o IsarCmd.init_toplevel)); 
5991  998 

24868  999 
val _ = 
8678  1000 
OuterSyntax.improper_command "welcome" "print welcome message" K.diag 
9010  1001 
(Scan.succeed (Toplevel.no_timing o IsarCmd.welcome)); 
7462  1002 

5832  1003 
end; 