author | wenzelm |
Tue, 02 Sep 2008 14:10:45 +0200 | |
changeset 28083 | 103d9282a946 |
parent 27816 | 0dfed2f2822a |
child 28084 | a05ca48ef263 |
permissions | -rw-r--r-- |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Isar/spec_parse.ML |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
3 |
Author: Makarius |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
4 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
5 |
Parsers for complex specifications. |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
6 |
*) |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
7 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
8 |
signature SPEC_PARSE = |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
9 |
sig |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
10 |
type token |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
11 |
val attrib: OuterLex.token list -> Attrib.src * token list |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
12 |
val attribs: token list -> Attrib.src list * token list |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
13 |
val opt_attribs: token list -> Attrib.src list * token list |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
14 |
val thm_name: string -> token list -> (Name.binding * Attrib.src list) * token list |
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
15 |
val opt_thm_name: string -> token list -> (Name.binding * Attrib.src list) * token list |
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
16 |
val spec: token list -> ((Name.binding * Attrib.src list) * string list) * token list |
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
17 |
val named_spec: token list -> ((Name.binding * Attrib.src list) * string list) * token list |
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
18 |
val spec_name: token list -> ((Name.binding * string) * Attrib.src list) * token list |
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
19 |
val spec_opt_name: token list -> ((Name.binding * string) * Attrib.src list) * token list |
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
25999
diff
changeset
|
20 |
val xthm: token list -> (Facts.ref * Attrib.src list) * token list |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
25999
diff
changeset
|
21 |
val xthms1: token list -> (Facts.ref * Attrib.src list) list * token list |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
22 |
val name_facts: token list -> |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
23 |
((Name.binding * Attrib.src list) * (Facts.ref * Attrib.src list) list) list * token list |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
24 |
val locale_mixfix: token list -> mixfix * token list |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
25 |
val locale_fixes: token list -> (Name.binding * string option * mixfix) list * token list |
25094
ba43514068fd
Interpretation equations may have name and/or attribute.
ballarin
parents:
24869
diff
changeset
|
26 |
val locale_insts: token list -> |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
27 |
(string option list * ((Name.binding * Attrib.src list) * string) list) * token list |
24869 | 28 |
val class_expr: token list -> string list * token list |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
29 |
val locale_expr: token list -> Locale.expr * token list |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
30 |
val locale_keyword: token list -> string * token list |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
31 |
val locale_element: token list -> Element.context Locale.element * token list |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
32 |
val context_element: token list -> Element.context * token list |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
33 |
val statement: token list -> |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
34 |
((Name.binding * Attrib.src list) * (string * string list) list) list * token list |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
35 |
val general_statement: token list -> |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
36 |
(Element.context Locale.element list * Element.statement) * OuterLex.token list |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
37 |
val statement_keyword: token list -> string * token list |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
38 |
val specification: token list -> |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
39 |
(Name.binding * |
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
40 |
(((Name.binding * Attrib.src list) * string list) list * |
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
41 |
(Name.binding * string option) list)) list * token list |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
42 |
end; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
43 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
44 |
structure SpecParse: SPEC_PARSE = |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
45 |
struct |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
46 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
47 |
structure P = OuterParse; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
48 |
type token = P.token; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
49 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
50 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
51 |
(* theorem specifications *) |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
52 |
|
27816
0dfed2f2822a
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset
|
53 |
val attrib = P.position ((P.keyword_ident_or_symbolic || P.xname) -- P.!!! Args.parse) >> Args.src; |
24014 | 54 |
val attribs = P.$$$ "[" |-- P.list attrib --| P.$$$ "]"; |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
55 |
val opt_attribs = Scan.optional attribs []; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
56 |
|
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
57 |
fun thm_name s = P.binding -- opt_attribs --| P.$$$ s; |
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
58 |
|
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
59 |
fun opt_thm_name s = |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
60 |
Scan.optional ((P.binding -- opt_attribs || attribs >> pair Name.no_binding) --| P.$$$ s) |
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
61 |
(Name.no_binding, []); |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
62 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
63 |
val spec = opt_thm_name ":" -- Scan.repeat1 P.prop; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
64 |
val named_spec = thm_name ":" -- Scan.repeat1 P.prop; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
65 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
66 |
val spec_name = thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y)); |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
67 |
val spec_opt_name = opt_thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y)); |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
68 |
|
24013
3063a756611d
xthm: added [[declaration]] syntax (abbreviates dummy_thm [att]);
wenzelm
parents:
23919
diff
changeset
|
69 |
val xthm = |
26361 | 70 |
P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.named "") || |
71 |
(P.alt_string >> Facts.Fact || |
|
27816
0dfed2f2822a
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset
|
72 |
P.position P.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs; |
24013
3063a756611d
xthm: added [[declaration]] syntax (abbreviates dummy_thm [att]);
wenzelm
parents:
23919
diff
changeset
|
73 |
|
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
74 |
val xthms1 = Scan.repeat1 xthm; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
75 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
76 |
val name_facts = P.and_list1 (opt_thm_name "=" -- xthms1); |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
77 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
78 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
79 |
(* locale and context elements *) |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
80 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
81 |
val locale_mixfix = P.$$$ "(" -- P.$$$ "structure" -- P.!!! (P.$$$ ")") >> K Structure || P.mixfix; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
82 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
83 |
val locale_fixes = |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
84 |
P.and_list1 (P.binding -- Scan.option (P.$$$ "::" |-- P.typ) -- locale_mixfix |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
85 |
>> (single o P.triple1) || |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
86 |
P.params >> map Syntax.no_syn) >> flat; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
87 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
88 |
val locale_insts = |
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22104
diff
changeset
|
89 |
Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) [] |
25094
ba43514068fd
Interpretation equations may have name and/or attribute.
ballarin
parents:
24869
diff
changeset
|
90 |
-- Scan.optional (P.$$$ "where" |-- P.and_list1 (opt_thm_name ":" -- P.prop)) []; |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
91 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
92 |
local |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
93 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
94 |
val loc_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" || |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
95 |
P.$$$ "defines" || P.$$$ "notes" || P.$$$ "includes"; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
96 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
97 |
val loc_element = |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
98 |
P.$$$ "fixes" |-- P.!!! locale_fixes >> Element.Fixes || |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
99 |
P.$$$ "constrains" |-- P.!!! (P.and_list1 (P.name -- (P.$$$ "::" |-- P.typ))) |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
100 |
>> Element.Constrains || |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
101 |
P.$$$ "assumes" |-- P.!!! (P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp)) |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
102 |
>> Element.Assumes || |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
103 |
P.$$$ "defines" |-- P.!!! (P.and_list1 (opt_thm_name ":" -- P.propp)) |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
104 |
>> Element.Defines || |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
105 |
P.$$$ "notes" |-- P.!!! (P.and_list1 (opt_thm_name "=" -- xthms1)) |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
106 |
>> (curry Element.Notes ""); |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
107 |
|
24869 | 108 |
fun plus1_unless test scan = |
25999 | 109 |
scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan)); |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
110 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
111 |
val rename = P.name -- Scan.option P.mixfix; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
112 |
|
24869 | 113 |
in |
114 |
||
115 |
val class_expr = plus1_unless loc_keyword P.xname; |
|
116 |
||
117 |
val locale_expr = |
|
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
118 |
let |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
119 |
fun expr2 x = (P.xname >> Locale.Locale || P.$$$ "(" |-- P.!!! (expr0 --| P.$$$ ")")) x |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
120 |
and expr1 x = (expr2 -- Scan.repeat1 (P.maybe rename) >> Locale.Rename || expr2) x |
24869 | 121 |
and expr0 x = (plus1_unless loc_keyword expr1 >> (fn [e] => e | es => Locale.Merge es)) x; |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
122 |
in expr0 end; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
123 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
124 |
val locale_keyword = loc_keyword; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
125 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
126 |
val locale_element = P.group "locale element" |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
127 |
(loc_element >> Locale.Elem || P.$$$ "includes" |-- P.!!! locale_expr >> Locale.Expr); |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
128 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
129 |
val context_element = P.group "context element" loc_element; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
130 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
131 |
end; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
132 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
133 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
134 |
(* statements *) |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
135 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
136 |
val statement = P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp); |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
137 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
138 |
val obtain_case = |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
139 |
P.parbinding -- (Scan.optional (P.simple_fixes --| P.$$$ "where") [] -- |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
140 |
(P.and_list1 (Scan.repeat1 P.prop) >> flat)); |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
141 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
142 |
val general_statement = |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
143 |
statement >> (fn x => ([], Element.Shows x)) || |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
144 |
Scan.repeat locale_element -- |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
145 |
(P.$$$ "obtains" |-- P.!!! (P.enum1 "|" obtain_case) >> Element.Obtains || |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
146 |
P.$$$ "shows" |-- P.!!! statement >> Element.Shows); |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
147 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
148 |
val statement_keyword = P.$$$ "obtains" || P.$$$ "shows"; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
149 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
150 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
151 |
(* specifications *) |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
152 |
|
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
153 |
val specification = P.enum1 "|" (P.parbinding -- (P.and_list1 spec -- P.for_simple_fixes)); |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
154 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
155 |
end; |