author | wenzelm |
Sat, 28 May 2016 21:38:58 +0200 | |
changeset 63178 | b9e1d53124f5 |
parent 63094 | 056ea294c256 |
child 63180 | ddfd021884b4 |
permissions | -rw-r--r-- |
36952
338c3f8229e4
renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents:
36950
diff
changeset
|
1 |
(* Title: Pure/Isar/parse_spec.ML |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
3 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
4 |
Parsers for complex specifications. |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
5 |
*) |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
6 |
|
36952
338c3f8229e4
renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents:
36950
diff
changeset
|
7 |
signature PARSE_SPEC = |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
8 |
sig |
29312 | 9 |
val thm_name: string -> Attrib.binding parser |
10 |
val opt_thm_name: string -> Attrib.binding parser |
|
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
56945
diff
changeset
|
11 |
val name_facts: (Attrib.binding * (Facts.ref * Token.src list) list) list parser |
63064
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
62969
diff
changeset
|
12 |
val simple_spec: (Attrib.binding * string) parser |
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
62969
diff
changeset
|
13 |
val simple_specs: (Attrib.binding * string list) parser |
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
62969
diff
changeset
|
14 |
val if_assumes: string list parser |
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
62969
diff
changeset
|
15 |
val spec: (string list * (Attrib.binding * string)) parser |
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
62969
diff
changeset
|
16 |
val multi_specs: Specification.multi_specs_cmd parser |
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
62969
diff
changeset
|
17 |
val where_multi_specs: Specification.multi_specs_cmd parser |
33287
0f99569d23e1
provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
wenzelm
parents:
30726
diff
changeset
|
18 |
val constdecl: (binding * string option * mixfix) parser |
47067
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
46922
diff
changeset
|
19 |
val includes: (xstring * Position.T) list parser |
29581 | 20 |
val locale_fixes: (binding * string option * mixfix) list parser |
29312 | 21 |
val locale_insts: (string option list * (Attrib.binding * string) list) parser |
46922
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
45592
diff
changeset
|
22 |
val class_expression: string list parser |
61606
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61466
diff
changeset
|
23 |
val locale_prefix: (string * bool) parser |
49754
acafcac41690
more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents:
47067
diff
changeset
|
24 |
val locale_keyword: string parser |
61606
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61466
diff
changeset
|
25 |
val locale_expression: Expression.expression parser |
29312 | 26 |
val context_element: Element.context parser |
61654
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61606
diff
changeset
|
27 |
val statement': (string * string list) list list parser |
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61606
diff
changeset
|
28 |
val if_statement': (string * string list) list list parser |
29312 | 29 |
val statement: (Attrib.binding * (string * string list) list) list parser |
60449 | 30 |
val if_statement: (Attrib.binding * (string * string list) list) list parser |
60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60449
diff
changeset
|
31 |
val cond_statement: (bool * (Attrib.binding * (string * string list) list) list) parser |
60448 | 32 |
val obtains: Element.obtains parser |
63094
056ea294c256
toplevel theorem statements support 'if'/'for' eigen-context;
wenzelm
parents:
63064
diff
changeset
|
33 |
val long_statement: (Element.context list * Element.statement) parser |
056ea294c256
toplevel theorem statements support 'if'/'for' eigen-context;
wenzelm
parents:
63064
diff
changeset
|
34 |
val long_statement_keyword: string parser |
61260 | 35 |
val overloaded: bool parser |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
36 |
end; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
37 |
|
36952
338c3f8229e4
renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents:
36950
diff
changeset
|
38 |
structure Parse_Spec: PARSE_SPEC = |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
39 |
struct |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
40 |
|
63064
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
62969
diff
changeset
|
41 |
(* simple specifications *) |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
42 |
|
58028
e4250d370657
tuned signature -- define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset
|
43 |
fun thm_name s = Parse.binding -- Parse.opt_attribs --| Parse.$$$ s; |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
44 |
|
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
45 |
fun opt_thm_name s = |
58028
e4250d370657
tuned signature -- define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset
|
46 |
Scan.optional |
e4250d370657
tuned signature -- define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset
|
47 |
((Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty) --| Parse.$$$ s) |
28965 | 48 |
Attrib.empty_binding; |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
49 |
|
63064
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
62969
diff
changeset
|
50 |
val simple_spec = opt_thm_name ":" -- Parse.prop; |
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
62969
diff
changeset
|
51 |
val simple_specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop; |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
52 |
|
62969 | 53 |
val name_facts = Parse.and_list1 (opt_thm_name "=" -- Parse.thms1); |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
54 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
55 |
|
63064
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
62969
diff
changeset
|
56 |
(* structured specifications *) |
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
62969
diff
changeset
|
57 |
|
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
62969
diff
changeset
|
58 |
val if_assumes = |
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
62969
diff
changeset
|
59 |
Scan.optional (Parse.$$$ "if" |-- Parse.!!! (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat)) |
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
62969
diff
changeset
|
60 |
[]; |
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
62969
diff
changeset
|
61 |
|
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
62969
diff
changeset
|
62 |
val spec = (opt_thm_name ":" -- Parse.prop) -- if_assumes >> swap; |
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
62969
diff
changeset
|
63 |
|
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
62969
diff
changeset
|
64 |
val multi_specs = |
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
62969
diff
changeset
|
65 |
Parse.enum1 "|" |
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
62969
diff
changeset
|
66 |
(opt_thm_name ":" -- Parse.prop -- if_assumes --| |
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
62969
diff
changeset
|
67 |
Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|"))); |
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
62969
diff
changeset
|
68 |
|
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
62969
diff
changeset
|
69 |
val where_multi_specs = Parse.where_ |-- Parse.!!! multi_specs; |
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
62969
diff
changeset
|
70 |
|
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
62969
diff
changeset
|
71 |
|
33287
0f99569d23e1
provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
wenzelm
parents:
30726
diff
changeset
|
72 |
(* basic constant specifications *) |
0f99569d23e1
provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
wenzelm
parents:
30726
diff
changeset
|
73 |
|
0f99569d23e1
provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
wenzelm
parents:
30726
diff
changeset
|
74 |
val constdecl = |
36950 | 75 |
Parse.binding -- |
76 |
(Parse.where_ >> K (NONE, NoSyn) || |
|
77 |
Parse.$$$ "::" |-- Parse.!!! ((Parse.typ >> SOME) -- Parse.opt_mixfix' --| Parse.where_) || |
|
78 |
Scan.ahead (Parse.$$$ "(") |-- Parse.!!! (Parse.mixfix' --| Parse.where_ >> pair NONE)) |
|
61466 | 79 |
>> Scan.triple2; |
33287
0f99569d23e1
provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
wenzelm
parents:
30726
diff
changeset
|
80 |
|
0f99569d23e1
provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
wenzelm
parents:
30726
diff
changeset
|
81 |
|
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
82 |
(* locale and context elements *) |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
83 |
|
62969 | 84 |
val includes = Parse.$$$ "includes" |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.name)); |
47067
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
46922
diff
changeset
|
85 |
|
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
86 |
val locale_fixes = |
51654
8450b944e58a
just one syntax category "mixfix" -- check structure annotation semantically;
wenzelm
parents:
49754
diff
changeset
|
87 |
Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- Parse.mixfix |
61466 | 88 |
>> (single o Scan.triple1) || |
60448 | 89 |
Parse.params) >> flat; |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
90 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
91 |
val locale_insts = |
36950 | 92 |
Scan.optional |
93 |
(Parse.$$$ "[" |-- Parse.!!! (Scan.repeat1 (Parse.maybe Parse.term) --| Parse.$$$ "]")) [] -- |
|
94 |
Scan.optional (Parse.where_ |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) []; |
|
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
95 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
96 |
local |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
97 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
98 |
val loc_element = |
36950 | 99 |
Parse.$$$ "fixes" |-- Parse.!!! locale_fixes >> Element.Fixes || |
100 |
Parse.$$$ "constrains" |-- |
|
101 |
Parse.!!! (Parse.and_list1 (Parse.name -- (Parse.$$$ "::" |-- Parse.typ))) |
|
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
102 |
>> Element.Constrains || |
36950 | 103 |
Parse.$$$ "assumes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp)) |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
104 |
>> Element.Assumes || |
36950 | 105 |
Parse.$$$ "defines" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Parse.propp)) |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
106 |
>> Element.Defines || |
62969 | 107 |
Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- Parse.thms1)) |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
108 |
>> (curry Element.Notes ""); |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
109 |
|
24869 | 110 |
fun plus1_unless test scan = |
36950 | 111 |
scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan)); |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
112 |
|
36950 | 113 |
val instance = Parse.where_ |-- |
114 |
Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named || |
|
115 |
Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional; |
|
29033
721529248e31
Enable keyword 'structure' in for clause of locale expression.
ballarin
parents:
28965
diff
changeset
|
116 |
|
24869 | 117 |
in |
118 |
||
61606
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61466
diff
changeset
|
119 |
val locale_prefix = |
49754
acafcac41690
more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents:
47067
diff
changeset
|
120 |
Scan.optional |
61606
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61466
diff
changeset
|
121 |
(Parse.name -- (Scan.option (Parse.$$$ "?") >> is_none) --| Parse.$$$ ":") |
49754
acafcac41690
more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents:
47067
diff
changeset
|
122 |
("", false); |
acafcac41690
more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents:
47067
diff
changeset
|
123 |
|
36950 | 124 |
val locale_keyword = |
125 |
Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" || |
|
126 |
Parse.$$$ "defines" || Parse.$$$ "notes"; |
|
28722 | 127 |
|
46922
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
45592
diff
changeset
|
128 |
val class_expression = plus1_unless locale_keyword Parse.class; |
24869 | 129 |
|
61606
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61466
diff
changeset
|
130 |
val locale_expression = |
29033
721529248e31
Enable keyword 'structure' in for clause of locale expression.
ballarin
parents:
28965
diff
changeset
|
131 |
let |
62969 | 132 |
val expr2 = Parse.position Parse.name; |
61606
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61466
diff
changeset
|
133 |
val expr1 = |
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61466
diff
changeset
|
134 |
locale_prefix -- expr2 -- |
30720 | 135 |
Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i))); |
136 |
val expr0 = plus1_unless locale_keyword expr1; |
|
36950 | 137 |
in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end; |
29033
721529248e31
Enable keyword 'structure' in for clause of locale expression.
ballarin
parents:
28965
diff
changeset
|
138 |
|
44357 | 139 |
val context_element = Parse.group (fn () => "context element") loc_element; |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
140 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
141 |
end; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
142 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
143 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
144 |
(* statements *) |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
145 |
|
61654
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61606
diff
changeset
|
146 |
val statement' = Parse.and_list1 (Scan.repeat1 Parse.propp); |
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61606
diff
changeset
|
147 |
val if_statement' = Scan.optional (Parse.$$$ "if" |-- Parse.!!! statement') []; |
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61606
diff
changeset
|
148 |
|
36950 | 149 |
val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp); |
60449 | 150 |
val if_statement = Scan.optional (Parse.$$$ "if" |-- Parse.!!! statement) []; |
60414 | 151 |
|
60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60449
diff
changeset
|
152 |
val cond_statement = |
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60449
diff
changeset
|
153 |
Parse.$$$ "if" |-- Parse.!!! statement >> pair true || |
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60449
diff
changeset
|
154 |
Parse.$$$ "when" |-- Parse.!!! statement >> pair false || |
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60449
diff
changeset
|
155 |
Scan.succeed (true, []); |
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60449
diff
changeset
|
156 |
|
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
157 |
val obtain_case = |
59784 | 158 |
Parse.parbinding -- |
60448 | 159 |
(Scan.optional (Parse.and_list1 Parse.fixes --| Parse.where_ >> flat) [] -- |
59784 | 160 |
(Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat)); |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
161 |
|
60448 | 162 |
val obtains = Parse.enum1 "|" obtain_case; |
163 |
||
63094
056ea294c256
toplevel theorem statements support 'if'/'for' eigen-context;
wenzelm
parents:
63064
diff
changeset
|
164 |
val long_statement = |
28722 | 165 |
Scan.repeat context_element -- |
60448 | 166 |
(Parse.$$$ "obtains" |-- Parse.!!! obtains >> Element.Obtains || |
36950 | 167 |
Parse.$$$ "shows" |-- Parse.!!! statement >> Element.Shows); |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
168 |
|
63094
056ea294c256
toplevel theorem statements support 'if'/'for' eigen-context;
wenzelm
parents:
63064
diff
changeset
|
169 |
val long_statement_keyword = |
056ea294c256
toplevel theorem statements support 'if'/'for' eigen-context;
wenzelm
parents:
63064
diff
changeset
|
170 |
locale_keyword || Parse.$$$ "obtains" || Parse.$$$ "shows"; |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
171 |
|
61260 | 172 |
|
173 |
(* options *) |
|
174 |
||
175 |
val overloaded = |
|
176 |
Scan.optional (Parse.$$$ "(" -- Parse.$$$ "overloaded" -- Parse.$$$ ")" >> K true) false; |
|
177 |
||
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
178 |
end; |