author | wenzelm |
Sat, 20 Oct 2007 18:54:34 +0200 | |
changeset 25121 | fbea3ca04d51 |
parent 25094 | ba43514068fd |
child 25999 | f8bcd311d501 |
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 |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
14 |
val thm_name: string -> token list -> (bstring * Attrib.src list) * token list |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
15 |
val opt_thm_name: string -> token list -> (bstring * Attrib.src list) * token list |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
16 |
val spec: token list -> ((bstring * Attrib.src list) * string list) * token list |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
17 |
val named_spec: token list -> ((bstring * Attrib.src list) * string list) * token list |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
18 |
val spec_name: token list -> ((bstring * string) * Attrib.src list) * token list |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
19 |
val spec_opt_name: token list -> ((bstring * string) * Attrib.src list) * token list |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
20 |
val xthm: token list -> (thmref * Attrib.src list) * token list |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
21 |
val xthms1: token list -> (thmref * Attrib.src list) list * token list |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
22 |
val name_facts: token list -> |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
23 |
((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list * token list |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
24 |
val locale_mixfix: token list -> mixfix * token list |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
25 |
val locale_fixes: token list -> (string * 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 -> |
ba43514068fd
Interpretation equations may have name and/or attribute.
ballarin
parents:
24869
diff
changeset
|
27 |
(string option list * ((bstring * 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 -> |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
34 |
((bstring * Attrib.src list) * (string * string list) list) list * token list |
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 -> |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
39 |
(string * |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
40 |
(((bstring * Attrib.src list) * string list) list * (string * string option) list)) list * |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
41 |
token list |
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 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
53 |
val attrib = P.position ((P.keyword_sid || P.xname) -- P.!!! P.arguments) >> 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 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
57 |
fun thm_name s = P.name -- opt_attribs --| P.$$$ s; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
58 |
fun opt_thm_name s = |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
59 |
Scan.optional ((P.name -- opt_attribs || (attribs >> pair "")) --| P.$$$ s) ("", []); |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
60 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
61 |
val spec = opt_thm_name ":" -- Scan.repeat1 P.prop; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
62 |
val named_spec = thm_name ":" -- Scan.repeat1 P.prop; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
63 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
64 |
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
|
65 |
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
|
66 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
67 |
val thm_sel = P.$$$ "(" |-- P.list1 |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
68 |
(P.nat --| P.minus -- P.nat >> PureThy.FromTo || |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
69 |
P.nat --| P.minus >> PureThy.From || |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
70 |
P.nat >> PureThy.Single) --| P.$$$ ")"; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
71 |
|
24013
3063a756611d
xthm: added [[declaration]] syntax (abbreviates dummy_thm [att]);
wenzelm
parents:
23919
diff
changeset
|
72 |
val xthm = |
3063a756611d
xthm: added [[declaration]] syntax (abbreviates dummy_thm [att]);
wenzelm
parents:
23919
diff
changeset
|
73 |
P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Name "") || |
3063a756611d
xthm: added [[declaration]] syntax (abbreviates dummy_thm [att]);
wenzelm
parents:
23919
diff
changeset
|
74 |
(P.alt_string >> Fact || P.xname -- thm_sel >> NameSelection || P.xname >> Name) -- opt_attribs; |
3063a756611d
xthm: added [[declaration]] syntax (abbreviates dummy_thm [att]);
wenzelm
parents:
23919
diff
changeset
|
75 |
|
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
76 |
val xthms1 = Scan.repeat1 xthm; |
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 |
val name_facts = P.and_list1 (opt_thm_name "=" -- xthms1); |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
79 |
|
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 |
(* locale and context elements *) |
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_mixfix = P.$$$ "(" -- P.$$$ "structure" -- P.!!! (P.$$$ ")") >> K Structure || P.mixfix; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
84 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
85 |
val locale_fixes = |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
86 |
P.and_list1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- locale_mixfix |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
87 |
>> (single o P.triple1) || |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
88 |
P.params >> map Syntax.no_syn) >> flat; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
89 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
90 |
val locale_insts = |
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22104
diff
changeset
|
91 |
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
|
92 |
-- 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
|
93 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
94 |
local |
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 |
val loc_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" || |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
97 |
P.$$$ "defines" || P.$$$ "notes" || P.$$$ "includes"; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
98 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
99 |
val loc_element = |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
100 |
P.$$$ "fixes" |-- P.!!! locale_fixes >> Element.Fixes || |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
101 |
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
|
102 |
>> Element.Constrains || |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
103 |
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
|
104 |
>> Element.Assumes || |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
105 |
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
|
106 |
>> Element.Defines || |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
107 |
P.$$$ "notes" |-- P.!!! (P.and_list1 (opt_thm_name "=" -- xthms1)) |
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 = |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
111 |
scan -- Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan)) >> op ::; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
112 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
113 |
val rename = P.name -- Scan.option P.mixfix; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
114 |
|
24869 | 115 |
in |
116 |
||
117 |
val class_expr = plus1_unless loc_keyword P.xname; |
|
118 |
||
119 |
val locale_expr = |
|
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
120 |
let |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
121 |
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
|
122 |
and expr1 x = (expr2 -- Scan.repeat1 (P.maybe rename) >> Locale.Rename || expr2) x |
24869 | 123 |
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
|
124 |
in expr0 end; |
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_keyword = loc_keyword; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
127 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
128 |
val locale_element = P.group "locale element" |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
129 |
(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
|
130 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
131 |
val context_element = P.group "context element" loc_element; |
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 |
end; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
134 |
|
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 |
(* statements *) |
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 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
|
139 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
140 |
val obtain_case = |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
141 |
P.parname -- (Scan.optional (P.simple_fixes --| P.$$$ "where") [] -- |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
142 |
(P.and_list1 (Scan.repeat1 P.prop) >> flat)); |
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 |
val general_statement = |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
145 |
statement >> (fn x => ([], Element.Shows x)) || |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
146 |
Scan.repeat locale_element -- |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
147 |
(P.$$$ "obtains" |-- P.!!! (P.enum1 "|" obtain_case) >> Element.Obtains || |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
148 |
P.$$$ "shows" |-- P.!!! statement >> Element.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 |
val statement_keyword = P.$$$ "obtains" || P.$$$ "shows"; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
151 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
152 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
153 |
(* specifications *) |
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 |
val specification = P.enum1 "|" (P.parname -- (P.and_list1 spec -- P.for_simple_fixes)); |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
156 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
157 |
end; |