author  ballarin 
Tue, 02 Sep 2008 17:31:20 +0200  
changeset 28085  914183e229e9 
parent 28084  a05ca48ef263 
child 28114  2637fb838f74 
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 

27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
27200
diff
changeset

19 
val _ = List.app OuterKeyword.keyword 
24868  20 
["!!", "!", "%", "(", ")", "+", ",", "", ":", "::", ";", "<", "<=", 
21 
"=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>", 

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

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

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

29 

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

24868  32 
val _ = 
17068  33 
OuterSyntax.command "theory" "begin theory" (K.tag_theory K.thy_begin) 
27575  34 
(ThyHeader.args >> (Toplevel.print oo IsarCmd.init_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 
27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

44 
(P.doc_source >> IsarCmd.header_markup); 
6353  45 

24868  46 
val _ = OuterSyntax.markup_command ThyOutput.Markup "chapter" "chapter heading" 
27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

47 
K.thy_heading (P.opt_target  P.doc_source >> IsarCmd.local_theory_markup); 
5958  48 

24868  49 
val _ = OuterSyntax.markup_command ThyOutput.Markup "section" "section heading" 
27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

50 
K.thy_heading (P.opt_target  P.doc_source >> IsarCmd.local_theory_markup); 
5958  51 

24868  52 
val _ = OuterSyntax.markup_command ThyOutput.Markup "subsection" "subsection heading" 
27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

53 
K.thy_heading (P.opt_target  P.doc_source >> IsarCmd.local_theory_markup); 
5958  54 

24868  55 
val _ = 
22117  56 
OuterSyntax.markup_command ThyOutput.Markup "subsubsection" "subsubsection heading" 
27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

57 
K.thy_heading (P.opt_target  P.doc_source >> IsarCmd.local_theory_markup); 
5832  58 

24868  59 
val _ = OuterSyntax.markup_command ThyOutput.MarkupEnv "text" "formal comment (theory)" 
27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

60 
K.thy_decl (P.opt_target  P.doc_source >> IsarCmd.local_theory_markup); 
7172  61 

27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

62 
val _ = OuterSyntax.markup_command ThyOutput.Verbatim "text_raw" "raw document preparation text" 
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

63 
K.thy_decl (P.opt_target  P.doc_source >> IsarCmd.local_theory_markup); 
7172  64 

24868  65 
val _ = OuterSyntax.markup_command ThyOutput.Markup "sect" "formal comment (proof)" 
27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

66 
(K.tag_proof K.prf_heading) (P.doc_source >> IsarCmd.proof_markup); 
7172  67 

24868  68 
val _ = OuterSyntax.markup_command ThyOutput.Markup "subsect" "formal comment (proof)" 
27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

69 
(K.tag_proof K.prf_heading) (P.doc_source >> IsarCmd.proof_markup); 
7172  70 

27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

71 
val _ = OuterSyntax.markup_command ThyOutput.Markup "subsubsect" "formal comment (proof)" 
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

72 
(K.tag_proof K.prf_heading) (P.doc_source >> IsarCmd.proof_markup); 
7172  73 

24868  74 
val _ = OuterSyntax.markup_command ThyOutput.MarkupEnv "txt" "formal comment (proof)" 
27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

75 
(K.tag_proof K.prf_decl) (P.doc_source >> IsarCmd.proof_markup); 
7172  76 

24868  77 
val _ = OuterSyntax.markup_command ThyOutput.Verbatim "txt_raw" 
17068  78 
"raw document preparation text (proof)" (K.tag_proof K.prf_decl) 
27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

79 
(P.doc_source >> IsarCmd.proof_markup); 
7775  80 

5832  81 

6886  82 

83 
(** theory sections **) 

84 

5832  85 
(* classes and sorts *) 
86 

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

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

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

24868  92 
val _ = 
6723  93 
OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl 
14779  94 
(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

95 
>> (Toplevel.theory o AxClass.axiomatize_classrel_cmd)); 
5832  96 

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

24868  101 
val _ = 
19245  102 
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

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

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

5832  108 

109 
(* types *) 

110 

24868  111 
val _ = 
12624  112 
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

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

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

119 
(P.type_args  P.name  (P.$$$ "="  P.!!! (P.typ  P.opt_infix'))) 
22796  120 
>> (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

121 
map (fn ((args, a), (T, mx)) => (a, args, T, mx)))); 
5832  122 

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

24868  127 
val _ = 
6723  128 
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

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

131 

132 
(* consts and syntax *) 

133 

24868  134 
val _ = 
8227  135 
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

136 
(P.const >> (Toplevel.theory o ObjectLogic.add_judgment)); 
8227  137 

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

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

143 

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

145 
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

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

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

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

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

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

5832  162 

163 
(* translations *) 

164 

165 
val trans_pat = 

6723  166 
Scan.optional (P.$$$ "("  P.!!! (P.xname  P.$$$ ")")) "logic"  P.string; 
5832  167 

168 
fun trans_arrow toks = 

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

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

5832  172 

173 
val trans_line = 

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

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

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

5832  185 

186 
(* axioms and definitions *) 

187 

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

19631  192 
val opt_unchecked_overloaded = 
193 
Scan.optional (P.$$$ "("  P.!!! 

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

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

196 

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

14642  202 

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

203 
(* old constdefs *) 
14642  204 

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

205 
val old_constdecl = 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27877
diff
changeset

206 
P.binding  P.where_ >> (fn x => (x, NONE, NoSyn))  
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27877
diff
changeset

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

208 
 Scan.option P.where_ >> P.triple1  
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27877
diff
changeset

209 
P.binding  (P.mixfix >> pair NONE)  Scan.option P.where_ >> P.triple2; 
19076  210 

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

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

215 

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

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

219 

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

220 

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

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

222 

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

223 
val constdecl = 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27877
diff
changeset

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

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

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

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

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

229 

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

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

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

234 
(constdef >> (fn args => #2 o Specification.definition_cmd args)); 
18780  235 

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

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

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

239 
>> (fn (mode, args) => Specification.abbreviation_cmd mode args)); 
19659  240 

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

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

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

244 
>> (fn (mode, args) => Specification.notation_cmd true mode args)); 
24950  245 

246 
val _ = 

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

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

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

249 
>> (fn (mode, args) => Specification.notation_cmd false mode args)); 
19076  250 

5832  251 

18616  252 
(* constant specifications *) 
253 

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

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

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

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

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

260 

5914  261 
(* theorems *) 
262 

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

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

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

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

267 
OuterSyntax.local_theory "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK); 
5914  268 

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

270 
OuterSyntax.local_theory "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK); 
5914  271 

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

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

274 
(P.and_list1 SpecParse.xthms1 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

275 
>> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.no_binding, flat args)])); 
9589  276 

5914  277 

5832  278 
(* name space entry path *) 
279 

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

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

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

293 

294 
(* use ML text *) 

295 

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

5832  299 

24868  300 
val _ = 
26490  301 
OuterSyntax.command "ML" "eval ML text (diagnostic)" (K.tag_ml K.thy_decl) 
27877  302 
(P.ML_source >> (fn (txt, pos) => 
26490  303 
Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt)))); 
7891  304 

24868  305 
val _ = 
26396  306 
OuterSyntax.command "ML_val" "eval ML text (diagnostic)" (K.tag_ml K.diag) 
27877  307 
(P.ML_source >> IsarCmd.ml_diag true); 
26396  308 

309 
val _ = 

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

27877  311 
(P.ML_source >> (Toplevel.no_timing oo IsarCmd.ml_diag false)); 
5832  312 

24868  313 
val _ = 
17068  314 
OuterSyntax.command "setup" "apply ML theory setup" (K.tag_ml K.thy_decl) 
27877  315 
(P.ML_source >> (Toplevel.theory o IsarCmd.generic_setup)); 
5832  316 

24868  317 
val _ = 
17068  318 
OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl) 
27877  319 
(P.name  P.!!! (P.$$$ "="  P.ML_source  P.text) 
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26248
diff
changeset

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

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

323 
OuterSyntax.local_theory "declaration" "generic ML declaration" (K.tag_ml K.thy_decl) 
27877  324 
(P.ML_source >> IsarCmd.declaration); 
22088  325 

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

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

328 
(P.name  (P.$$$ "("  P.enum1 "" P.term  P.$$$ ")"  P.$$$ "=")  
27877  329 
P.ML_source  Scan.optional (P.$$$ "identifier"  Scan.repeat1 P.xname) [] 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

330 
>> (fn (((a, b), c), d) => IsarCmd.simproc_setup a b c d)); 
22202  331 

5832  332 

333 
(* translation functions *) 

334 

27877  335 
val trfun = P.opt_keyword "advanced"  P.ML_source; 
14642  336 

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

22117  340 
(trfun >> (Toplevel.theory o IsarCmd.parse_ast_translation)); 
5832  341 

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

22117  345 
(trfun >> (Toplevel.theory o IsarCmd.parse_translation)); 
5832  346 

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

22117  350 
(trfun >> (Toplevel.theory o IsarCmd.print_translation)); 
5832  351 

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

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

22117  360 
(trfun >> (Toplevel.theory o IsarCmd.print_ast_translation)); 
5832  361 

362 

363 
(* oracles *) 

364 

24868  365 
val _ = 
17068  366 
OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl) 
27877  367 
(P.name  (P.$$$ "("  P.ML_source  P.$$$ ")"  P.$$$ "=") 
368 
 P.ML_source >> (fn ((x, y), z) => Toplevel.theory (IsarCmd.oracle x y z))); 

5832  369 

370 

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

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

372 

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

374 
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

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

377 

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

378 

12061  379 
(* locales *) 
380 

12758  381 
val locale_val = 
24868  382 
SpecParse.locale_expr  
22117  383 
Scan.optional (P.$$$ "+"  P.!!! (Scan.repeat1 SpecParse.context_element)) []  
24868  384 
Scan.repeat1 SpecParse.context_element >> pair Locale.empty; 
12061  385 

24868  386 
val _ = 
12061  387 
OuterSyntax.command "locale" "define named proof context" K.thy_decl 
27681  388 
(P.name  Scan.optional (P.$$$ "="  P.!!! locale_val) (Locale.empty, [])  P.opt_begin 
389 
>> (fn ((name, (expr, elems)), begin) => 

21843  390 
(begin ? Toplevel.print) o Toplevel.begin_local_theory begin 
27681  391 
(Locale.add_locale "" name expr elems #> TheoryTarget.begin))); 
12061  392 

28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

393 
val opt_prefix = Scan.optional (P.binding  P.$$$ ":") Name.no_binding; 
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

394 

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

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

397 
"prove and register interpretation of locale expression in theory or locale" K.thy_goal 
22117  398 
(P.xname  (P.$$$ "\\<subseteq>"  P.$$$ "<")  P.!!! SpecParse.locale_expr 
20365  399 
>> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I))  
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

400 
opt_prefix  SpecParse.locale_expr  SpecParse.locale_insts 
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

401 
>> (fn ((name, expr), insts) => Toplevel.print o 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27877
diff
changeset

402 
Toplevel.theory_to_proof 
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

403 
(Locale.interpretation I (true, Name.name_of name) expr insts))); 
12061  404 

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

406 
OuterSyntax.command "interpret" 
17068  407 
"prove and register interpretation of locale expression in proof context" 
408 
(K.tag_proof K.prf_goal) 

28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

409 
(opt_prefix  SpecParse.locale_expr  SpecParse.locale_insts 
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

410 
>> (fn ((name, expr), insts) => Toplevel.print o 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27877
diff
changeset

411 
Toplevel.proof' 
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

412 
(Locale.interpret Seq.single (true, Name.name_of name) expr insts))); 
15703  413 

414 

22299  415 
(* classes *) 
416 

24868  417 
val class_val = 
418 
SpecParse.class_expr  

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

22299  421 

24868  422 
val _ = 
423 
OuterSyntax.command "class" "define type class" K.thy_decl 

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

24938  426 
(begin ? Toplevel.print) o Toplevel.begin_local_theory begin 
26516  427 
(Class.class_cmd name supclasses elems #> TheoryTarget.begin))); 
22299  428 

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

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

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

432 

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

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

24589  438 

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

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

27113  442 
P.arity >> Class.instance_arity_cmd) 
25485  443 
>> (Toplevel.print oo Toplevel.theory_to_proof) 
444 
 Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I))); 

22299  445 

446 

25519  447 
(* arbitrary overloading *) 
448 

449 
val _ = 

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

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

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

456 

457 

22866  458 
(* code generation *) 
459 

24868  460 
val _ = 
22866  461 
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

462 
(Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd)); 
22866  463 

464 

5832  465 

466 
(** proof commands **) 

467 

468 
(* statements *) 

469 

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

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

472 
(Scan.optional (SpecParse.opt_thm_name ":"  
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

473 
Scan.ahead (SpecParse.locale_keyword  SpecParse.statement_keyword)) Attrib.no_binding  
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

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

475 
(Specification.theorem_cmd kind NONE (K I) a elems concl))); 
5832  476 

24868  477 
val _ = gen_theorem Thm.theoremK; 
478 
val _ = gen_theorem Thm.lemmaK; 

479 
val _ = gen_theorem Thm.corollaryK; 

5832  480 

24868  481 
val _ = 
17353  482 
OuterSyntax.command "have" "state local goal" 
483 
(K.tag_proof K.prf_goal) 

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

24868  486 
val _ = 
17353  487 
OuterSyntax.command "hence" "abbreviates \"then have\"" 
488 
(K.tag_proof K.prf_goal) 

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

24868  491 
val _ = 
17068  492 
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

493 
(K.tag_proof K.prf_asm_goal) 
22117  494 
(SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show)); 
5832  495 

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

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

5832  501 

5914  502 
(* facts *) 
5832  503 

22117  504 
val facts = P.and_list1 SpecParse.xthms1; 
9197  505 

24868  506 
val _ = 
17068  507 
OuterSyntax.command "then" "forward chaining" 
508 
(K.tag_proof K.prf_chain) 

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

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

17900  514 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss))); 
5914  515 

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

17900  519 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss))); 
6878  520 

24868  521 
val _ = 
17068  522 
OuterSyntax.command "note" "define facts" 
523 
(K.tag_proof K.prf_decl) 

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

24868  526 
val _ = 
17068  527 
OuterSyntax.command "using" "augment goal facts" 
528 
(K.tag_proof K.prf_decl) 

18544  529 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.using))); 
530 

24868  531 
val _ = 
18544  532 
OuterSyntax.command "unfolding" "unfold definitions in goal and facts" 
533 
(K.tag_proof K.prf_decl) 

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

12926  535 

5832  536 

537 
(* proof context *) 

538 

24868  539 
val _ = 
17068  540 
OuterSyntax.command "fix" "fix local variables (Skolem constants)" 
541 
(K.tag_proof K.prf_asm) 

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

24868  544 
val _ = 
17068  545 
OuterSyntax.command "assume" "assume propositions" 
546 
(K.tag_proof K.prf_asm) 

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

24868  549 
val _ = 
17068  550 
OuterSyntax.command "presume" "assume propositions, to be established later" 
551 
(K.tag_proof K.prf_asm) 

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

24868  554 
val _ = 
17068  555 
OuterSyntax.command "def" "local definition" 
556 
(K.tag_proof K.prf_asm) 

18308  557 
(P.and_list1 
22117  558 
(SpecParse.opt_thm_name ":"  
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27877
diff
changeset

559 
((P.binding  P.opt_mixfix)  ((P.$$$ "\\<equiv>"  P.$$$ "==")  P.!!! P.termp))) 
18308  560 
>> (Toplevel.print oo (Toplevel.proof o Proof.def))); 
6953  561 

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

24868  568 
val _ = 
17854  569 
OuterSyntax.command "guess" "wild guessing (unstructured)" 
570 
(K.tag_proof K.prf_asm_goal) 

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

24868  573 
val _ = 
17068  574 
OuterSyntax.command "let" "bind text variables" 
575 
(K.tag_proof K.prf_decl) 

27378  576 
(P.and_list1 (P.and_list1 P.term  (P.$$$ "="  P.term)) 
17900  577 
>> (Toplevel.print oo (Toplevel.proof o Proof.let_bind))); 
5832  578 

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

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

582 

24868  583 
val _ = 
17068  584 
OuterSyntax.command "case" "invoke local context" 
585 
(K.tag_proof K.prf_asm) 

17900  586 
(case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case))); 
8370  587 

5832  588 

589 
(* proof structure *) 

590 

24868  591 
val _ = 
17068  592 
OuterSyntax.command "{" "begin explicit proof block" 
593 
(K.tag_proof K.prf_open) 

17900  594 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block)); 
5832  595 

24868  596 
val _ = 
17068  597 
OuterSyntax.command "}" "end explicit proof block" 
598 
(K.tag_proof K.prf_close) 

20305  599 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block)); 
6687  600 

24868  601 
val _ = 
17068  602 
OuterSyntax.command "next" "enter next proof block" 
603 
(K.tag_proof K.prf_block) 

17900  604 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block)); 
5832  605 

606 

607 
(* end proof *) 

608 

24868  609 
val _ = 
17068  610 
OuterSyntax.command "qed" "conclude (sub)proof" 
611 
(K.tag_proof K.qed_block) 

26676  612 
(Scan.option Method.parse >> IsarCmd.qed); 
5832  613 

24868  614 
val _ = 
17068  615 
OuterSyntax.command "by" "terminal backward proof" 
616 
(K.tag_proof K.qed) 

26676  617 
(Method.parse  Scan.option Method.parse >> IsarCmd.terminal_proof); 
6404  618 

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

26676  622 
(Scan.succeed IsarCmd.default_proof); 
8966  623 

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

26676  627 
(Scan.succeed IsarCmd.immediate_proof); 
6404  628 

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

26676  632 
(Scan.succeed IsarCmd.done_proof); 
5832  633 

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

638 

24868  639 
val _ = 
17068  640 
OuterSyntax.command "oops" "forget proof" 
641 
(K.tag_proof K.qed_global) 

18561  642 
(Scan.succeed Toplevel.forget_proof); 
8210  643 

5832  644 

645 
(* proof steps *) 

646 

24868  647 
val _ = 
17068  648 
OuterSyntax.command "defer" "shuffle internal proof state" 
649 
(K.tag_proof K.prf_script) 

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

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

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

24868  657 
val _ = 
17068  658 
OuterSyntax.command "apply" "initial refinement step (unstructured)" 
659 
(K.tag_proof K.prf_script) 

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

24868  662 
val _ = 
17068  663 
OuterSyntax.command "apply_end" "terminal refinement (unstructured)" 
664 
(K.tag_proof K.prf_script) 

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

24868  667 
val _ = 
17068  668 
OuterSyntax.command "proof" "backward proof" 
669 
(K.tag_proof K.prf_block) 

22117  670 
(Scan.option Method.parse >> (fn m => Toplevel.print o 
27563  671 
Toplevel.actual_proof (ProofNode.applys (Proof.proof m)) o 
672 
Toplevel.skip_proof (fn i => i + 1))); 

5832  673 

674 

6773  675 
(* calculational proof commands *) 
676 

6878  677 
val calc_args = 
22117  678 
Scan.option (P.$$$ "("  P.!!! ((SpecParse.xthms1  P.$$$ ")"))); 
6878  679 

24868  680 
val _ = 
17068  681 
OuterSyntax.command "also" "combine calculation and current facts" 
682 
(K.tag_proof K.prf_decl) 

17900  683 
(calc_args >> (Toplevel.proofs' o Calculation.also)); 
6773  684 

24868  685 
val _ = 
17068  686 
OuterSyntax.command "finally" "combine calculation and current facts, exhibit result" 
687 
(K.tag_proof K.prf_chain) 

22573  688 
(calc_args >> (Toplevel.proofs' o Calculation.finally_)); 
6773  689 

24868  690 
val _ = 
17068  691 
OuterSyntax.command "moreover" "augment calculation by current facts" 
692 
(K.tag_proof K.prf_decl) 

17900  693 
(Scan.succeed (Toplevel.proof' Calculation.moreover)); 
8562  694 

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

6773  700 

6742  701 
(* proof navigation *) 
5944  702 

24868  703 
val _ = 
17068  704 
OuterSyntax.command "back" "backtracking of proof command" 
705 
(K.tag_proof K.prf_script) 

27563  706 
(Scan.succeed (Toplevel.print o Toplevel.actual_proof ProofNode.back o Toplevel.skip_proof I)); 
6742  707 

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

708 

27614
f38c25d106a7
renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
wenzelm
parents:
27575
diff
changeset

709 
(* nested commands *) 
25578  710 

27719
de34a576c756
Isar.command: explicitly set transaction position, as required for prepare_command errors;
wenzelm
parents:
27681
diff
changeset

711 
val props_text = 
de34a576c756
Isar.command: explicitly set transaction position, as required for prepare_command errors;
wenzelm
parents:
27681
diff
changeset

712 
Scan.optional P.properties []  P.position P.string >> (fn (props, (str, pos)) => 
de34a576c756
Isar.command: explicitly set transaction position, as required for prepare_command errors;
wenzelm
parents:
27681
diff
changeset

713 
(Position.of_properties (Position.default_properties pos props), str)); 
de34a576c756
Isar.command: explicitly set transaction position, as required for prepare_command errors;
wenzelm
parents:
27681
diff
changeset

714 

25578  715 
val _ = 
716 
OuterSyntax.improper_command "Isabelle.command" "nested Isabelle command" K.control 

27719
de34a576c756
Isar.command: explicitly set transaction position, as required for prepare_command errors;
wenzelm
parents:
27681
diff
changeset

717 
(props_text : (fn (pos, str) => 
27838
0340fd7cccc3
Isabelle.command: inline former OuterSyntax.prepare_command;
wenzelm
parents:
27831
diff
changeset

718 
(case OuterSyntax.parse pos str of 
0340fd7cccc3
Isabelle.command: inline former OuterSyntax.prepare_command;
wenzelm
parents:
27831
diff
changeset

719 
[tr] => Scan.succeed (K tr) 
0340fd7cccc3
Isabelle.command: inline former OuterSyntax.prepare_command;
wenzelm
parents:
27831
diff
changeset

720 
 _ => Scan.fail_with (K "exactly one command expected")) 
0340fd7cccc3
Isabelle.command: inline former OuterSyntax.prepare_command;
wenzelm
parents:
27831
diff
changeset

721 
handle ERROR msg => Scan.fail_with (K msg))); 
25578  722 

723 

27563  724 
(* global history commands *) 
27525
ee2721e9e900
added Isar.undo, which emulates oldstyle undo on global tty state;
wenzelm
parents:
27494
diff
changeset

725 

ee2721e9e900
added Isar.undo, which emulates oldstyle undo on global tty state;
wenzelm
parents:
27494
diff
changeset

726 
val _ = 
27617
dee36037a832
added Isar.command, Isar.insert, Isar.remove (editor model);
wenzelm
parents:
27614
diff
changeset

727 
OuterSyntax.improper_command "Isar.command" "define command (Isar editor model)" K.control 
27719
de34a576c756
Isar.command: explicitly set transaction position, as required for prepare_command errors;
wenzelm
parents:
27681
diff
changeset

728 
(props_text >> (fn (pos, str) => 
27827
03ed3519cf48
Isar.command: do not set position of enclosing transaction, to avoid of clash with the one being prepared here!
wenzelm
parents:
27719
diff
changeset

729 
Toplevel.no_timing o Toplevel.imperative (fn () => 
27838
0340fd7cccc3
Isabelle.command: inline former OuterSyntax.prepare_command;
wenzelm
parents:
27831
diff
changeset

730 
ignore (Isar.create_command (OuterSyntax.prepare_command pos str))))); 
27617
dee36037a832
added Isar.command, Isar.insert, Isar.remove (editor model);
wenzelm
parents:
27614
diff
changeset

731 

dee36037a832
added Isar.command, Isar.insert, Isar.remove (editor model);
wenzelm
parents:
27614
diff
changeset

732 
val _ = 
dee36037a832
added Isar.command, Isar.insert, Isar.remove (editor model);
wenzelm
parents:
27614
diff
changeset

733 
OuterSyntax.improper_command "Isar.insert" "insert command (Isar editor model)" K.control 
dee36037a832
added Isar.command, Isar.insert, Isar.remove (editor model);
wenzelm
parents:
27614
diff
changeset

734 
(P.string  P.string >> (fn (prev, id) => 
dee36037a832
added Isar.command, Isar.insert, Isar.remove (editor model);
wenzelm
parents:
27614
diff
changeset

735 
Toplevel.no_timing o Toplevel.imperative (fn () => Isar.insert_command prev id))); 
dee36037a832
added Isar.command, Isar.insert, Isar.remove (editor model);
wenzelm
parents:
27614
diff
changeset

736 

dee36037a832
added Isar.command, Isar.insert, Isar.remove (editor model);
wenzelm
parents:
27614
diff
changeset

737 
val _ = 
dee36037a832
added Isar.command, Isar.insert, Isar.remove (editor model);
wenzelm
parents:
27614
diff
changeset

738 
OuterSyntax.improper_command "Isar.remove" "remove command (Isar editor model)" K.control 
dee36037a832
added Isar.command, Isar.insert, Isar.remove (editor model);
wenzelm
parents:
27614
diff
changeset

739 
(P.string >> (fn id => 
dee36037a832
added Isar.command, Isar.insert, Isar.remove (editor model);
wenzelm
parents:
27614
diff
changeset

740 
Toplevel.no_timing o Toplevel.imperative (fn () => Isar.remove_command id))); 
dee36037a832
added Isar.command, Isar.insert, Isar.remove (editor model);
wenzelm
parents:
27614
diff
changeset

741 

dee36037a832
added Isar.command, Isar.insert, Isar.remove (editor model);
wenzelm
parents:
27614
diff
changeset

742 
val _ = 
27534
048294b251ee
activated new versions of init_toplevel, linear_undo, undo, undos_proof kill;
wenzelm
parents:
27531
diff
changeset

743 
OuterSyntax.improper_command "init_toplevel" "init toplevel pointofinterest" K.control 
27531  744 
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.init_point)); 
745 

746 
val _ = 

27534
048294b251ee
activated new versions of init_toplevel, linear_undo, undo, undos_proof kill;
wenzelm
parents:
27531
diff
changeset

747 
OuterSyntax.improper_command "linear_undo" "undo commands" K.control 
27529  748 
(Scan.optional P.nat 1 >> 
749 
(fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.linear_undo n))); 

750 

751 
val _ = 

27534
048294b251ee
activated new versions of init_toplevel, linear_undo, undo, undos_proof kill;
wenzelm
parents:
27531
diff
changeset

752 
OuterSyntax.improper_command "undo" "undo commands (skipping closed proofs)" K.control 
27525
ee2721e9e900
added Isar.undo, which emulates oldstyle undo on global tty state;
wenzelm
parents:
27494
diff
changeset

753 
(Scan.optional P.nat 1 >> 
ee2721e9e900
added Isar.undo, which emulates oldstyle undo on global tty state;
wenzelm
parents:
27494
diff
changeset

754 
(fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo n))); 
ee2721e9e900
added Isar.undo, which emulates oldstyle undo on global tty state;
wenzelm
parents:
27494
diff
changeset

755 

27531  756 
val _ = 
27534
048294b251ee
activated new versions of init_toplevel, linear_undo, undo, undos_proof kill;
wenzelm
parents:
27531
diff
changeset

757 
OuterSyntax.improper_command "undos_proof" "undo commands (skipping closed proofs)" K.control 
048294b251ee
activated new versions of init_toplevel, linear_undo, undo, undos_proof kill;
wenzelm
parents:
27531
diff
changeset

758 
(Scan.optional P.nat 1 >> (fn n => Toplevel.no_timing o 
048294b251ee
activated new versions of init_toplevel, linear_undo, undo, undos_proof kill;
wenzelm
parents:
27531
diff
changeset

759 
Toplevel.keep (fn state => 
048294b251ee
activated new versions of init_toplevel, linear_undo, undo, undos_proof kill;
wenzelm
parents:
27531
diff
changeset

760 
if Toplevel.is_proof state then (Isar.undo n; Isar.print ()) else raise Toplevel.UNDEF))); 
048294b251ee
activated new versions of init_toplevel, linear_undo, undo, undos_proof kill;
wenzelm
parents:
27531
diff
changeset

761 

048294b251ee
activated new versions of init_toplevel, linear_undo, undo, undos_proof kill;
wenzelm
parents:
27531
diff
changeset

762 
val _ = 
27563  763 
OuterSyntax.improper_command "cannot_undo" "partial undo  Proof General legacy" K.control 
764 
(P.name >> 

765 
(fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1) 

766 
 txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt)))); 

767 

768 
val _ = 

27534
048294b251ee
activated new versions of init_toplevel, linear_undo, undo, undos_proof kill;
wenzelm
parents:
27531
diff
changeset

769 
OuterSyntax.improper_command "kill" "kill partial proof or theory development" K.control 
27531  770 
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.kill)); 
771 

27525
ee2721e9e900
added Isar.undo, which emulates oldstyle undo on global tty state;
wenzelm
parents:
27494
diff
changeset

772 

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

773 

5832  774 
(** diagnostic commands (for interactive mode only) **) 
775 

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

24868  779 
val _ = 
7124  780 
OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing" 
9010  781 
K.diag (P.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin)); 
7124  782 

24868  783 
val _ = 
21714  784 
OuterSyntax.improper_command "help" "print outer syntax commands" K.diag 
24871  785 
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative OuterSyntax.print_outer_syntax)); 
21714  786 

24868  787 
val _ = 
21714  788 
OuterSyntax.improper_command "print_commands" "print outer syntax commands" K.diag 
24871  789 
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative OuterSyntax.print_outer_syntax)); 
5832  790 

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

23989  794 

24868  795 
val _ = 
7308  796 
OuterSyntax.improper_command "print_context" "print theory context name" K.diag 
9010  797 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_context)); 
7308  798 

24868  799 
val _ = 
6723  800 
OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag 
20621  801 
(opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory)); 
5832  802 

24868  803 
val _ = 
21726  804 
OuterSyntax.improper_command "print_syntax" "print inner syntax of context (verbose!)" K.diag 
9010  805 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax)); 
5832  806 

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

810 

24868  811 
val _ = 
17068  812 
OuterSyntax.improper_command "print_theorems" 
813 
"print theorems of local theory or proof context" K.diag 

9010  814 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_theorems)); 
5881  815 

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

819 

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

821 
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

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

824 

24868  825 
val _ = 
15596  826 
OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag 
20621  827 
(opt_bang  locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale)); 
12061  828 

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

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

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

15596  834 

24868  835 
val _ = 
12061  836 
OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag 
9010  837 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes)); 
5832  838 

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

842 

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

846 

24868  847 
val _ = 
11666  848 
OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" K.diag 
9221  849 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules)); 
850 

24868  851 
val _ = 
12061  852 
OuterSyntax.improper_command "print_methods" "print methods of this theory" K.diag 
9010  853 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods)); 
5832  854 

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

858 

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

862 

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

866 

24868  867 
val _ = 
9454  868 
OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies" 
22117  869 
K.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps)); 
9454  870 

22866  871 
local 
872 

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

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

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

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

16074  878 
P.reserved "simp"  P.!!! (P.$$$ ":"  P.term) >> FindTheorems.Simp  
16027  879 
P.term >> FindTheorems.Pattern; 
880 

22866  881 
val options = 
882 
Scan.optional 

883 
(P.$$$ "("  

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

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

886 
in 

887 

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

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

892 

22866  893 
end; 
894 

24868  895 
val _ = 
6723  896 
OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag 
9010  897 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds)); 
5832  898 

24868  899 
val _ = 
8370  900 
OuterSyntax.improper_command "print_facts" "print facts of proof context" K.diag 
21004  901 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_facts)); 
5832  902 

24868  903 
val _ = 
8370  904 
OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag 
9010  905 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases)); 
8370  906 

24868  907 
val _ = 
19269  908 
OuterSyntax.improper_command "print_statement" "print theorems as long statements" K.diag 
22117  909 
(opt_modes  SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts)); 
19269  910 

24868  911 
val _ = 
8464  912 
OuterSyntax.improper_command "thm" "print theorems" K.diag 
22117  913 
(opt_modes  SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms)); 
5832  914 

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

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

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

919 

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

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

923 

24868  924 
val _ = 
6723  925 
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

926 
(opt_modes  P.term >> (Toplevel.no_timing oo IsarCmd.print_prop)); 
5832  927 

24868  928 
val _ = 
6723  929 
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

930 
(opt_modes  P.term >> (Toplevel.no_timing oo IsarCmd.print_term)); 
5832  931 

24868  932 
val _ = 
6723  933 
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

934 
(opt_modes  P.typ >> (Toplevel.no_timing oo IsarCmd.print_type)); 
5832  935 

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

937 
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

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

939 
(Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep 
24219  940 
(Code.print_codesetup o Toplevel.theory_of))); 
5832  941 

26184  942 
val _ = 
943 
OuterSyntax.improper_command "unused_thms" "find unused theorems" K.diag 

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

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

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

947 

5832  948 

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

950 

24868  951 
val _ = 
8650  952 
OuterSyntax.improper_command "cd" "change current working directory" K.diag 
14950  953 
(P.path >> (Toplevel.no_timing oo IsarCmd.cd)); 
5832  954 

24868  955 
val _ = 
6723  956 
OuterSyntax.improper_command "pwd" "print current working directory" K.diag 
9010  957 
(Scan.succeed (Toplevel.no_timing o IsarCmd.pwd)); 
5832  958 

24868  959 
val _ = 
6723  960 
OuterSyntax.improper_command "use_thy" "use theory file" K.diag 
26404  961 
(P.name >> (fn name => 
962 
Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.use_thy name))); 

5832  963 

24868  964 
val _ = 
7102  965 
OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag 
27494  966 
(P.name >> (fn name => 
967 
Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.touch_thy name))); 

7908  968 

24868  969 
val _ = 
7102  970 
OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag 
27494  971 
(P.name >> (fn name => 
972 
Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.remove_thy name))); 

7102  973 

24868  974 
val _ = 
7931  975 
OuterSyntax.improper_command "kill_thy" "kill theory  try to remove from loader database" 
27494  976 
K.diag (P.name >> (fn name => 
977 
Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.kill_thy name))); 

7931  978 

24868  979 
val _ = 
14934  980 
OuterSyntax.improper_command "display_drafts" "display raw source files with symbols" 
14950  981 
K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.display_drafts)); 
14934  982 

24868  983 
val _ = 
14934  984 
OuterSyntax.improper_command "print_drafts" "print raw source files with symbols" 
14950  985 
K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.print_drafts)); 
14934  986 

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

989 

24868  990 
val _ = 
8886  991 
OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag 
9731  992 
(opt_modes  opt_limits >> (Toplevel.no_timing oo IsarCmd.pr)); 
7199  993 

24868  994 
val _ = 
7222  995 
OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" K.diag 
9010  996 
(Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr)); 
5832  997 

24868  998 
val _ = 
7222  999 
OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag 
9010  1000 
(Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr)); 
7222  1001 

24868  1002 
val _ = 
6723  1003 
OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag 
26490  1004 
(P.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit)); 
5832  1005 

24868  1006 
val _ = 
6723  1007 
OuterSyntax.improper_command "quit" "quit Isabelle" K.control 
9010  1008 
(P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit)); 
5832  1009 

24868  1010 
val _ = 
6723  1011 
OuterSyntax.improper_command "exit" "exit Isar loop" K.control 
9010  1012 
(Scan.succeed (Toplevel.no_timing o IsarCmd.exit)); 
5832  1013 

24868  1014 
val _ = 
8678  1015 
OuterSyntax.improper_command "welcome" "print welcome message" K.diag 
9010  1016 
(Scan.succeed (Toplevel.no_timing o IsarCmd.welcome)); 
7462  1017 

5832  1018 
end; 
27614
f38c25d106a7
renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
wenzelm
parents:
27575
diff
changeset

1019 