author  wenzelm 
Mon, 05 Nov 2007 20:50:43 +0100  
changeset 25290  250c7a0205ca 
parent 25269  f9090ae5cec9 
child 25462  dad0291cb76a 
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) => 
22796  116 
Toplevel.theory (Sign.add_typedecls [(a, args, mx)]))); 
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 _ = 
24868  448 
OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal 
449 
((P.xname  ((P.$$$ "\\<subseteq>"  P.$$$ "<")  P.!!! P.xname) >> Class.classrel_cmd  

450 
P.and_list1 P.arity  Scan.repeat (SpecParse.opt_thm_name ":"  P.prop) 

451 
>> (fn (arities, defs) => Class.instance_cmd arities defs (fold Code.add_default_func (* FIXME ? *)))) 

452 
>> (Toplevel.print oo Toplevel.theory_to_proof)); 

22299  453 

24868  454 
val _ = 
455 
OuterSyntax.command "instantiation" "prove type arity" K.thy_decl 

456 
(P.and_list1 P.arity  P.opt_begin 

457 
>> (fn (arities, begin) => (begin ? Toplevel.print) o 

458 
Toplevel.begin_local_theory begin (Instance.begin_instantiation_cmd arities))); 

24589  459 

24868  460 
val _ = (* FIXME incorporate into "instance" *) 
24589  461 
OuterSyntax.command "instance_proof" "prove type arity relation" K.thy_goal 
24868  462 
(Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE Instance.proof_instantiation)); 
22299  463 

464 

22866  465 
(* code generation *) 
466 

24868  467 
val _ = 
22866  468 
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

469 
(Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd)); 
22866  470 

471 

5832  472 

473 
(** proof commands **) 

474 

475 
(* statements *) 

476 

17353  477 
fun gen_theorem kind = 
478 
OuterSyntax.command kind ("state " ^ kind) K.thy_goal 

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

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

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

483 
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

484 
(Specification.theorem_cmd kind NONE (K I) a elems concl)))); 
5832  485 

24868  486 
val _ = gen_theorem Thm.theoremK; 
487 
val _ = gen_theorem Thm.lemmaK; 

488 
val _ = gen_theorem Thm.corollaryK; 

5832  489 

24868  490 
val _ = 
17353  491 
OuterSyntax.command "have" "state local goal" 
492 
(K.tag_proof K.prf_goal) 

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

24868  495 
val _ = 
17353  496 
OuterSyntax.command "hence" "abbreviates \"then have\"" 
497 
(K.tag_proof K.prf_goal) 

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

24868  500 
val _ = 
17068  501 
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

502 
(K.tag_proof K.prf_asm_goal) 
22117  503 
(SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show)); 
5832  504 

24868  505 
val _ = 
17068  506 
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

507 
(K.tag_proof K.prf_asm_goal) 
22117  508 
(SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus)); 
6501  509 

5832  510 

5914  511 
(* facts *) 
5832  512 

22117  513 
val facts = P.and_list1 SpecParse.xthms1; 
9197  514 

24868  515 
val _ = 
17068  516 
OuterSyntax.command "then" "forward chaining" 
517 
(K.tag_proof K.prf_chain) 

17900  518 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain)); 
5832  519 

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

17900  523 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss))); 
5914  524 

24868  525 
val _ = 
17068  526 
OuterSyntax.command "with" "forward chaining from given and current facts" 
527 
(K.tag_proof K.prf_chain) 

17900  528 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss))); 
6878  529 

24868  530 
val _ = 
17068  531 
OuterSyntax.command "note" "define facts" 
532 
(K.tag_proof K.prf_decl) 

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

24868  535 
val _ = 
17068  536 
OuterSyntax.command "using" "augment goal facts" 
537 
(K.tag_proof K.prf_decl) 

18544  538 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.using))); 
539 

24868  540 
val _ = 
18544  541 
OuterSyntax.command "unfolding" "unfold definitions in goal and facts" 
542 
(K.tag_proof K.prf_decl) 

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

12926  544 

5832  545 

546 
(* proof context *) 

547 

24868  548 
val _ = 
17068  549 
OuterSyntax.command "fix" "fix local variables (Skolem constants)" 
550 
(K.tag_proof K.prf_asm) 

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

24868  553 
val _ = 
17068  554 
OuterSyntax.command "assume" "assume propositions" 
555 
(K.tag_proof K.prf_asm) 

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

24868  558 
val _ = 
17068  559 
OuterSyntax.command "presume" "assume propositions, to be established later" 
560 
(K.tag_proof K.prf_asm) 

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

24868  563 
val _ = 
17068  564 
OuterSyntax.command "def" "local definition" 
565 
(K.tag_proof K.prf_asm) 

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

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

24868  577 
val _ = 
17854  578 
OuterSyntax.command "guess" "wild guessing (unstructured)" 
579 
(K.tag_proof K.prf_asm_goal) 

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

24868  582 
val _ = 
17068  583 
OuterSyntax.command "let" "bind text variables" 
584 
(K.tag_proof K.prf_decl) 

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

585 
(P.and_list1 (P.enum1 "and" P.term  (P.$$$ "="  P.term)) 
17900  586 
>> (Toplevel.print oo (Toplevel.proof o Proof.let_bind))); 
5832  587 

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

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

591 

24868  592 
val _ = 
17068  593 
OuterSyntax.command "case" "invoke local context" 
594 
(K.tag_proof K.prf_asm) 

17900  595 
(case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case))); 
8370  596 

5832  597 

598 
(* proof structure *) 

599 

24868  600 
val _ = 
17068  601 
OuterSyntax.command "{" "begin explicit proof block" 
602 
(K.tag_proof K.prf_open) 

17900  603 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block)); 
5832  604 

24868  605 
val _ = 
17068  606 
OuterSyntax.command "}" "end explicit proof block" 
607 
(K.tag_proof K.prf_close) 

20305  608 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block)); 
6687  609 

24868  610 
val _ = 
17068  611 
OuterSyntax.command "next" "enter next proof block" 
612 
(K.tag_proof K.prf_block) 

17900  613 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block)); 
5832  614 

615 

616 
(* end proof *) 

617 

24868  618 
val _ = 
17068  619 
OuterSyntax.command "qed" "conclude (sub)proof" 
620 
(K.tag_proof K.qed_block) 

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

24868  623 
val _ = 
17068  624 
OuterSyntax.command "by" "terminal backward proof" 
625 
(K.tag_proof K.qed) 

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

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

21350  631 
(Scan.succeed (Toplevel.print3 o IsarCmd.default_proof)); 
8966  632 

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

21350  636 
(Scan.succeed (Toplevel.print3 o IsarCmd.immediate_proof)); 
6404  637 

24868  638 
val _ = 
17068  639 
OuterSyntax.command "done" "done proof" 
640 
(K.tag_proof K.qed) 

21350  641 
(Scan.succeed (Toplevel.print3 o IsarCmd.done_proof)); 
5832  642 

24868  643 
val _ = 
25108  644 
OuterSyntax.command "sorry" "skip proof (quickanddirty mode only!)" 
17068  645 
(K.tag_proof K.qed) 
21350  646 
(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

647 

24868  648 
val _ = 
17068  649 
OuterSyntax.command "oops" "forget proof" 
650 
(K.tag_proof K.qed_global) 

18561  651 
(Scan.succeed Toplevel.forget_proof); 
8210  652 

5832  653 

654 
(* proof steps *) 

655 

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

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

24868  661 
val _ = 
17068  662 
OuterSyntax.command "prefer" "shuffle internal proof state" 
663 
(K.tag_proof K.prf_script) 

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

24868  666 
val _ = 
17068  667 
OuterSyntax.command "apply" "initial refinement step (unstructured)" 
668 
(K.tag_proof K.prf_script) 

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

24868  671 
val _ = 
17068  672 
OuterSyntax.command "apply_end" "terminal refinement (unstructured)" 
673 
(K.tag_proof K.prf_script) 

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

24868  676 
val _ = 
17068  677 
OuterSyntax.command "proof" "backward proof" 
678 
(K.tag_proof K.prf_block) 

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

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

681 
Toplevel.skip_proof (History.apply (fn i => i + 1)))); 
5832  682 

683 

6773  684 
(* calculational proof commands *) 
685 

6878  686 
val calc_args = 
22117  687 
Scan.option (P.$$$ "("  P.!!! ((SpecParse.xthms1  P.$$$ ")"))); 
6878  688 

24868  689 
val _ = 
17068  690 
OuterSyntax.command "also" "combine calculation and current facts" 
691 
(K.tag_proof K.prf_decl) 

17900  692 
(calc_args >> (Toplevel.proofs' o Calculation.also)); 
6773  693 

24868  694 
val _ = 
17068  695 
OuterSyntax.command "finally" "combine calculation and current facts, exhibit result" 
696 
(K.tag_proof K.prf_chain) 

22573  697 
(calc_args >> (Toplevel.proofs' o Calculation.finally_)); 
6773  698 

24868  699 
val _ = 
17068  700 
OuterSyntax.command "moreover" "augment calculation by current facts" 
701 
(K.tag_proof K.prf_decl) 

17900  702 
(Scan.succeed (Toplevel.proof' Calculation.moreover)); 
8562  703 

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

6773  709 

6742  710 
(* proof navigation *) 
5944  711 

24868  712 
val _ = 
17068  713 
OuterSyntax.command "back" "backtracking of proof command" 
714 
(K.tag_proof K.prf_script) 

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

5832  716 

717 

6742  718 
(* history *) 
719 

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

6742  723 

24868  724 
val _ = 
6742  725 
OuterSyntax.improper_command "redo" "redo last command" K.control 
9010  726 
(Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.redo)); 
6742  727 

24868  728 
val _ = 
6742  729 
OuterSyntax.improper_command "undos_proof" "undo last proof commands" K.control 
9010  730 
(P.nat >> ((Toplevel.no_timing o Toplevel.print) oo IsarCmd.undos_proof)); 
6742  731 

24868  732 
val _ = 
6742  733 
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

734 
(Scan.succeed (Toplevel.no_timing o IsarCmd.undo)); 
6742  735 

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

739 

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

740 

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

741 

5832  742 
(** diagnostic commands (for interactive mode only) **) 
743 

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

24868  747 
val _ = 
7124  748 
OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing" 
9010  749 
K.diag (P.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin)); 
7124  750 

24868  751 
val _ = 
21714  752 
OuterSyntax.improper_command "help" "print outer syntax commands" K.diag 
24871  753 
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative OuterSyntax.print_outer_syntax)); 
21714  754 

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

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

23989  762 

24868  763 
val _ = 
7308  764 
OuterSyntax.improper_command "print_context" "print theory context name" K.diag 
9010  765 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_context)); 
7308  766 

24868  767 
val _ = 
6723  768 
OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag 
20621  769 
(opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory)); 
5832  770 

24868  771 
val _ = 
21726  772 
OuterSyntax.improper_command "print_syntax" "print inner syntax of context (verbose!)" K.diag 
9010  773 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax)); 
5832  774 

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

778 

24868  779 
val _ = 
17068  780 
OuterSyntax.improper_command "print_theorems" 
781 
"print theorems of local theory or proof context" K.diag 

9010  782 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_theorems)); 
5881  783 

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

787 

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

789 
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

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

792 

24868  793 
val _ = 
15596  794 
OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag 
20621  795 
(opt_bang  locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale)); 
12061  796 

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

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

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

15596  802 

24868  803 
val _ = 
12061  804 
OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag 
9010  805 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes)); 
5832  806 

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

810 

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

814 

24868  815 
val _ = 
11666  816 
OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" K.diag 
9221  817 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules)); 
818 

24868  819 
val _ = 
12061  820 
OuterSyntax.improper_command "print_methods" "print methods of this theory" K.diag 
9010  821 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods)); 
5832  822 

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

826 

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

830 

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

834 

24868  835 
val _ = 
9454  836 
OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies" 
22117  837 
K.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps)); 
9454  838 

22866  839 
local 
840 

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

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

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

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

16074  846 
P.reserved "simp"  P.!!! (P.$$$ ":"  P.term) >> FindTheorems.Simp  
16027  847 
P.term >> FindTheorems.Pattern; 
848 

22866  849 
val options = 
850 
Scan.optional 

851 
(P.$$$ "("  

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

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

854 
in 

855 

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

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

860 

22866  861 
end; 
862 

24868  863 
val _ = 
6723  864 
OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag 
9010  865 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds)); 
5832  866 

24868  867 
val _ = 
8370  868 
OuterSyntax.improper_command "print_facts" "print facts of proof context" K.diag 
21004  869 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_facts)); 
5832  870 

24868  871 
val _ = 
8370  872 
OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag 
9010  873 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases)); 
8370  874 

24868  875 
val _ = 
19269  876 
OuterSyntax.improper_command "print_statement" "print theorems as long statements" K.diag 
22117  877 
(opt_modes  SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts)); 
19269  878 

24868  879 
val _ = 
8464  880 
OuterSyntax.improper_command "thm" "print theorems" K.diag 
22117  881 
(opt_modes  SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms)); 
5832  882 

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

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

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

887 

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

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

891 

24868  892 
val _ = 
6723  893 
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

894 
(opt_modes  P.term >> (Toplevel.no_timing oo IsarCmd.print_prop)); 
5832  895 

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

898 
(opt_modes  P.term >> (Toplevel.no_timing oo IsarCmd.print_term)); 
5832  899 

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

902 
(opt_modes  P.typ >> (Toplevel.no_timing oo IsarCmd.print_type)); 
5832  903 

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

905 
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

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

907 
(Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep 
24219  908 
(Code.print_codesetup o Toplevel.theory_of))); 
5832  909 

910 

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

912 

24868  913 
val _ = 
8650  914 
OuterSyntax.improper_command "cd" "change current working directory" K.diag 
14950  915 
(P.path >> (Toplevel.no_timing oo IsarCmd.cd)); 
5832  916 

24868  917 
val _ = 
6723  918 
OuterSyntax.improper_command "pwd" "print current working directory" K.diag 
9010  919 
(Scan.succeed (Toplevel.no_timing o IsarCmd.pwd)); 
5832  920 

24868  921 
val _ = 
6723  922 
OuterSyntax.improper_command "use_thy" "use theory file" K.diag 
9010  923 
(P.name >> (Toplevel.no_timing oo IsarCmd.use_thy)); 
5832  924 

24868  925 
val _ = 
7102  926 
OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag 
9010  927 
(P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy)); 
7102  928 

24868  929 
val _ = 
7908  930 
OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag 
9010  931 
(P.name >> (Toplevel.no_timing oo IsarCmd.touch_child_thys)); 
7908  932 

24868  933 
val _ = 
7102  934 
OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag 
9010  935 
(P.name >> (Toplevel.no_timing oo IsarCmd.remove_thy)); 
7102  936 

24868  937 
val _ = 
7931  938 
OuterSyntax.improper_command "kill_thy" "kill theory  try to remove from loader database" 
9010  939 
K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.kill_thy)); 
7931  940 

24868  941 
val _ = 
14934  942 
OuterSyntax.improper_command "display_drafts" "display raw source files with symbols" 
14950  943 
K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.display_drafts)); 
14934  944 

24868  945 
val _ = 
14934  946 
OuterSyntax.improper_command "print_drafts" "print raw source files with symbols" 
14950  947 
K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.print_drafts)); 
14934  948 

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

951 

24868  952 
val _ = 
8886  953 
OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag 
9731  954 
(opt_modes  opt_limits >> (Toplevel.no_timing oo IsarCmd.pr)); 
7199  955 

24868  956 
val _ = 
7222  957 
OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" K.diag 
9010  958 
(Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr)); 
5832  959 

24868  960 
val _ = 
7222  961 
OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag 
9010  962 
(Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr)); 
7222  963 

24868  964 
val _ = 
6723  965 
OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag 
9010  966 
(P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.use_commit)); 
5832  967 

24868  968 
val _ = 
6723  969 
OuterSyntax.improper_command "quit" "quit Isabelle" K.control 
9010  970 
(P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit)); 
5832  971 

24868  972 
val _ = 
6723  973 
OuterSyntax.improper_command "exit" "exit Isar loop" K.control 
9010  974 
(Scan.succeed (Toplevel.no_timing o IsarCmd.exit)); 
5832  975 

24868  976 
val _ = 
7102  977 
OuterSyntax.improper_command "init_toplevel" "restart Isar toplevel loop" K.control 
9010  978 
(Scan.succeed (Toplevel.no_timing o IsarCmd.init_toplevel)); 
5991  979 

24868  980 
val _ = 
8678  981 
OuterSyntax.improper_command "welcome" "print welcome message" K.diag 
9010  982 
(Scan.succeed (Toplevel.no_timing o IsarCmd.welcome)); 
7462  983 

5832  984 
end; 