author  haftmann 
Mon, 08 Oct 2007 22:03:21 +0200  
changeset 24914  95cda5dd58d5 
parent 24871  6af56e53734a 
child 24932  86ef9a828a9e 
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", 

26 
"local_syntax", "notes", "obtains", "open", "output", "overloaded", "shows", 

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.$$$ "<")  
19516  92 
P.!!! (P.list1 P.xname)) []) >> (Toplevel.theory o fold AxClass.axiomatize_class)); 
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)) 
19516  97 
>> (Toplevel.theory o AxClass.axiomatize_classrel)); 
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 
22331  131 
(Scan.repeat1 P.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity)); 
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 = 
154 
Scan.optional (P.$$$ "("  P.!!! (mode_spec  P.$$$ ")")) Syntax.default_mode; 

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 
18949  237 
>> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.definition 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) => 
21527  243 
Toplevel.local_theory loc (Specification.abbreviation mode args))); 
19659  244 

24868  245 
val _ = 
21210  246 
OuterSyntax.command "notation" "variable/constant syntax" K.thy_decl 
22117  247 
(P.opt_target  opt_mode  P.and_list1 (P.xname  P.mixfix) 
19659  248 
>> (fn ((loc, mode), args) => 
21210  249 
Toplevel.local_theory loc (Specification.notation mode args))); 
19076  250 

5832  251 

18616  252 
(* constant specifications *) 
253 

24868  254 
val _ = 
18616  255 
OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl 
22117  256 
(P.opt_target  
18949  257 
(Scan.optional P.fixes []  
22117  258 
Scan.optional (P.where_  P.!!! (P.and_list1 SpecParse.spec)) []) 
18949  259 
>> (fn (loc, (x, y)) => Toplevel.local_theory loc (#2 o Specification.axiomatization x y))); 
18616  260 

261 

5914  262 
(* theorems *) 
263 

22117  264 
fun theorems kind = P.opt_target  SpecParse.name_facts 
20907  265 
>> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.theorems kind args)); 
12712  266 

24868  267 
val _ = 
21437  268 
OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK); 
5914  269 

24868  270 
val _ = 
21437  271 
OuterSyntax.command "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK); 
5914  272 

24868  273 
val _ = 
23795  274 
OuterSyntax.command "declare" "declare theorems (improper)" K.thy_decl 
22117  275 
(P.opt_target  (P.and_list1 SpecParse.xthms1 >> flat) 
20907  276 
>> (fn (loc, args) => Toplevel.local_theory loc 
277 
(#2 o Specification.theorems "" [(("", []), args)]))); 

9589  278 

5914  279 

5832  280 
(* name space entry path *) 
281 

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

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

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

5832  294 

295 

296 
(* use ML text *) 

297 

24868  298 
val _ = 
17068  299 
OuterSyntax.command "use" "eval ML text from file" (K.tag_ml K.diag) 
14950  300 
(P.path >> (Toplevel.no_timing oo IsarCmd.use)); 
5832  301 

24868  302 
val _ = 
17068  303 
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

304 
(P.text >> IsarCmd.use_mltext true); 
7891  305 

24868  306 
val _ = 
17068  307 
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

308 
(P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false)); 
7616  309 

24868  310 
val _ = 
17068  311 
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

312 
(P.text >> IsarCmd.use_mltext_theory); 
5832  313 

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

24868  318 
val _ = 
17068  319 
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

320 
(((P.name  P.!!! (P.$$$ "="  P.text  P.text) >> P.triple2)) 
17353  321 
>> (Toplevel.theory o Method.method_setup)); 
9197  322 

24868  323 
val _ = 
22088  324 
OuterSyntax.command "declaration" "generic ML declaration" (K.tag_ml K.thy_decl) 
22117  325 
(P.opt_target  P.text 
22088  326 
>> (fn (loc, txt) => Toplevel.local_theory loc (IsarCmd.declaration txt))); 
327 

24868  328 
val _ = 
22202  329 
OuterSyntax.command "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl) 
330 
(P.opt_target  

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

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

22202  334 

5832  335 

336 
(* translation functions *) 

337 

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

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

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

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

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

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

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

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

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

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

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

22117  368 
(P.text >> (Toplevel.theory o IsarCmd.token_translation)); 
5832  369 

370 

371 
(* oracles *) 

372 

24868  373 
val _ = 
17068  374 
OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl) 
16849  375 
(P.name  (P.$$$ "("  P.text  P.$$$ ")"  P.$$$ "=") 
22239  376 
 P.text >> (fn ((x, y), z) => Toplevel.theory (IsarCmd.oracle x y z))); 
5832  377 

378 

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

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

380 

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

382 
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

383 
(P.name  P.begin >> (fn name => 
7ab6e95e6b0b
turned 'context' into plain thy_decl, discontinued thy_switch;
wenzelm
parents:
21269
diff
changeset

384 
Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.init (SOME name)))); 
7ab6e95e6b0b
turned 'context' into plain thy_decl, discontinued thy_switch;
wenzelm
parents:
21269
diff
changeset

385 

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

386 

12061  387 
(* locales *) 
388 

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

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

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

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

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

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

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

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

12061  410 

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

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

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

15703  418 

419 

22299  420 
(* classes *) 
421 

24868  422 
val class_val = 
423 
SpecParse.class_expr  

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

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

22299  426 

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

429 
(P.name  

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

431 
Scan.optional (P.$$$ "("  (P.$$$ "local_syntax" >> K true)  P.$$$ ")") false  (* FIXME ?? *) 

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

24748  433 
>> (fn ((((bname, add_consts), local_syntax), (supclasses, elems)), begin) => 
22299  434 
Toplevel.begin_local_theory begin 
24748  435 
(Class.class_cmd false bname supclasses elems add_consts #> TheoryTarget.begin))); 
22299  436 

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

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

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

440 
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

441 

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

442 
val _ = 
24868  443 
OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal 
444 
((P.xname  ((P.$$$ "\\<subseteq>"  P.$$$ "<")  P.!!! P.xname) >> Class.classrel_cmd  

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

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

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

22299  448 

24868  449 
val _ = 
450 
OuterSyntax.command "instantiation" "prove type arity" K.thy_decl 

451 
(P.and_list1 P.arity  P.opt_begin 

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

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

24589  454 

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

459 

22866  460 
(* code generation *) 
461 

24868  462 
val _ = 
22866  463 
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

464 
(Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd)); 
22866  465 

466 

5832  467 

468 
(** proof commands **) 

469 

470 
(* statements *) 

471 

17353  472 
fun gen_theorem kind = 
473 
OuterSyntax.command kind ("state " ^ kind) K.thy_goal 

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

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

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

478 
Toplevel.local_theory_to_proof' loc 
21228  479 
(Specification.theorem kind NONE (K I) a elems concl)))); 
5832  480 

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

483 
val _ = gen_theorem Thm.corollaryK; 

5832  484 

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

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

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

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

24868  495 
val _ = 
17068  496 
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

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

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

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

5832  505 

5914  506 
(* facts *) 
5832  507 

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

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

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

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

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

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

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

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

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

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

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

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

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

12926  539 

5832  540 

541 
(* proof context *) 

542 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

586 

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

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

5832  592 

593 
(* proof structure *) 

594 

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

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

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

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

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

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

610 

611 
(* end proof *) 

612 

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

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

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

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

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

21350  626 
(Scan.succeed (Toplevel.print3 o IsarCmd.default_proof)); 
8966  627 

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

21350  631 
(Scan.succeed (Toplevel.print3 o IsarCmd.immediate_proof)); 
6404  632 

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

21350  636 
(Scan.succeed (Toplevel.print3 o IsarCmd.done_proof)); 
5832  637 

24868  638 
val _ = 
17068  639 
OuterSyntax.improper_command "sorry" "skip proof (quickanddirty mode only!)" 
640 
(K.tag_proof K.qed) 

21350  641 
(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

642 

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

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

5832  648 

649 
(* proof steps *) 

650 

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

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

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

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

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

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

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

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

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

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

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

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

678 

6773  679 
(* calculational proof commands *) 
680 

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

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

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

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

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

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

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

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

6773  704 

6742  705 
(* proof navigation *) 
5944  706 

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

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

5832  711 

712 

6742  713 
(* history *) 
714 

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

6742  718 

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

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

24868  727 
val _ = 
6742  728 
OuterSyntax.improper_command "undo" "undo last command" K.control 
22866  729 
(Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.undo)); 
6742  730 

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

734 

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

735 

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

736 

5832  737 
(** diagnostic commands (for interactive mode only) **) 
738 

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

24868  742 
val _ = 
7124  743 
OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing" 
9010  744 
K.diag (P.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin)); 
7124  745 

24868  746 
val _ = 
21714  747 
OuterSyntax.improper_command "help" "print outer syntax commands" K.diag 
24871  748 
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative OuterSyntax.print_outer_syntax)); 
21714  749 

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

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

23989  757 

24868  758 
val _ = 
7308  759 
OuterSyntax.improper_command "print_context" "print theory context name" K.diag 
9010  760 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_context)); 
7308  761 

24868  762 
val _ = 
6723  763 
OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag 
20621  764 
(opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory)); 
5832  765 

24868  766 
val _ = 
21726  767 
OuterSyntax.improper_command "print_syntax" "print inner syntax of context (verbose!)" K.diag 
9010  768 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax)); 
5832  769 

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

773 

24868  774 
val _ = 
17068  775 
OuterSyntax.improper_command "print_theorems" 
776 
"print theorems of local theory or proof context" K.diag 

9010  777 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_theorems)); 
5881  778 

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

782 

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

784 
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

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

787 

24868  788 
val _ = 
15596  789 
OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag 
20621  790 
(opt_bang  locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale)); 
12061  791 

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

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

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

15596  797 

24868  798 
val _ = 
12061  799 
OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag 
9010  800 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes)); 
5832  801 

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

805 

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

809 

24868  810 
val _ = 
11666  811 
OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" K.diag 
9221  812 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules)); 
813 

24868  814 
val _ = 
12061  815 
OuterSyntax.improper_command "print_methods" "print methods of this theory" K.diag 
9010  816 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods)); 
5832  817 

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

821 

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

825 

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

829 

24868  830 
val _ = 
9454  831 
OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies" 
22117  832 
K.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps)); 
9454  833 

22866  834 
local 
835 

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

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

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

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

16074  841 
P.reserved "simp"  P.!!! (P.$$$ ":"  P.term) >> FindTheorems.Simp  
16027  842 
P.term >> FindTheorems.Pattern; 
843 

22866  844 
val options = 
845 
Scan.optional 

846 
(P.$$$ "("  

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

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

849 
in 

850 

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

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

855 

22866  856 
end; 
857 

24868  858 
val _ = 
6723  859 
OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag 
9010  860 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds)); 
5832  861 

24868  862 
val _ = 
8370  863 
OuterSyntax.improper_command "print_facts" "print facts of proof context" K.diag 
21004  864 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_facts)); 
5832  865 

24868  866 
val _ = 
8370  867 
OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag 
9010  868 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases)); 
8370  869 

24868  870 
val _ = 
19269  871 
OuterSyntax.improper_command "print_statement" "print theorems as long statements" K.diag 
22117  872 
(opt_modes  SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts)); 
19269  873 

24868  874 
val _ = 
8464  875 
OuterSyntax.improper_command "thm" "print theorems" K.diag 
22117  876 
(opt_modes  SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms)); 
5832  877 

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

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

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

882 

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

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

886 

24868  887 
val _ = 
6723  888 
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

889 
(opt_modes  P.term >> (Toplevel.no_timing oo IsarCmd.print_prop)); 
5832  890 

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

893 
(opt_modes  P.term >> (Toplevel.no_timing oo IsarCmd.print_term)); 
5832  894 

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

897 
(opt_modes  P.typ >> (Toplevel.no_timing oo IsarCmd.print_type)); 
5832  898 

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

900 
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

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

902 
(Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep 
24219  903 
(Code.print_codesetup o Toplevel.theory_of))); 
5832  904 

905 

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

907 

24868  908 
val _ = 
8650  909 
OuterSyntax.improper_command "cd" "change current working directory" K.diag 
14950  910 
(P.path >> (Toplevel.no_timing oo IsarCmd.cd)); 
5832  911 

24868  912 
val _ = 
6723  913 
OuterSyntax.improper_command "pwd" "print current working directory" K.diag 
9010  914 
(Scan.succeed (Toplevel.no_timing o IsarCmd.pwd)); 
5832  915 

24868  916 
val _ = 
6723  917 
OuterSyntax.improper_command "use_thy" "use theory file" K.diag 
9010  918 
(P.name >> (Toplevel.no_timing oo IsarCmd.use_thy)); 
5832  919 

24868  920 
val _ = 
7102  921 
OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag 
9010  922 
(P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy)); 
7102  923 

24868  924 
val _ = 
7908  925 
OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag 
9010  926 
(P.name >> (Toplevel.no_timing oo IsarCmd.touch_child_thys)); 
7908  927 

24868  928 
val _ = 
7102  929 
OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag 
9010  930 
(P.name >> (Toplevel.no_timing oo IsarCmd.remove_thy)); 
7102  931 

24868  932 
val _ = 
7931  933 
OuterSyntax.improper_command "kill_thy" "kill theory  try to remove from loader database" 
9010  934 
K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.kill_thy)); 
7931  935 

24868  936 
val _ = 
14934  937 
OuterSyntax.improper_command "display_drafts" "display raw source files with symbols" 
14950  938 
K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.display_drafts)); 
14934  939 

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

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

946 

24868  947 
val _ = 
8886  948 
OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag 
9731  949 
(opt_modes  opt_limits >> (Toplevel.no_timing oo IsarCmd.pr)); 
7199  950 

24868  951 
val _ = 
7222  952 
OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" K.diag 
9010  953 
(Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr)); 
5832  954 

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

24868  959 
val _ = 
6723  960 
OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag 
9010  961 
(P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.use_commit)); 
5832  962 

24868  963 
val _ = 
6723  964 
OuterSyntax.improper_command "quit" "quit Isabelle" K.control 
9010  965 
(P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit)); 
5832  966 

24868  967 
val _ = 
6723  968 
OuterSyntax.improper_command "exit" "exit Isar loop" K.control 
9010  969 
(Scan.succeed (Toplevel.no_timing o IsarCmd.exit)); 
5832  970 

24868  971 
val _ = 
7102  972 
OuterSyntax.improper_command "init_toplevel" "restart Isar toplevel loop" K.control 
9010  973 
(Scan.succeed (Toplevel.no_timing o IsarCmd.init_toplevel)); 
5991  974 

24868  975 
val _ = 
8678  976 
OuterSyntax.improper_command "welcome" "print welcome message" K.diag 
9010  977 
(Scan.succeed (Toplevel.no_timing o IsarCmd.welcome)); 
7462  978 

5832  979 
end; 