equal
deleted
inserted
replaced
40 struct |
40 struct |
41 |
41 |
42 type src = Args.src; |
42 type src = Args.src; |
43 |
43 |
44 |
44 |
45 |
|
46 (** named attributes **) |
45 (** named attributes **) |
47 |
46 |
48 (* theory data *) |
47 (* theory data *) |
49 |
48 |
50 structure AttributesData = TheoryDataFun |
49 structure AttributesData = TheoryDataFun |
185 |
184 |
186 (** basic attributes **) |
185 (** basic attributes **) |
187 |
186 |
188 (* configuration options *) |
187 (* configuration options *) |
189 |
188 |
190 fun option x = |
189 local |
191 syntax (Scan.lift (Args.name -- (Args.$$$ "=" |-- Args.name)) |
190 |
192 >> (fn (name, value) => Thm.declaration_attribute (K (Config.put_generic_src name value)))) x; |
191 val equals = Args.$$$ "="; |
|
192 |
|
193 fun scan_value (Config.Bool _) = |
|
194 (equals -- Args.$$$ "false") >> K (Config.Bool false) || |
|
195 (equals -- Args.$$$ "true") >> K (Config.Bool true) || |
|
196 (Scan.succeed (Config.Bool true)) |
|
197 | scan_value (Config.Int _) = (equals |-- Args.int) >> Config.Int |
|
198 | scan_value (Config.String _) = (equals |-- Args.name) >> Config.String; |
|
199 |
|
200 fun scan_config x = |
|
201 ((Args.name >> Config.the_config) :-- (fn (config, config_type) => |
|
202 scan_value config_type >> (fn value => |
|
203 K (Thm.declaration_attribute (K (Config.put_generic config value))))) >> #2) x; |
|
204 |
|
205 fun scan_att x = |
|
206 (Args.internal_attribute || |
|
207 (Scan.ahead (scan_config --| Args.terminator) :-- |
|
208 (fn att => Args.named_attribute (K att))) >> #2) x; |
|
209 |
|
210 in |
|
211 |
|
212 fun option x = syntax (Scan.lift ((scan_att >> Morphism.form) --| Scan.many Args.not_eof)) x; |
|
213 |
|
214 end; |
193 |
215 |
194 |
216 |
195 (* tags *) |
217 (* tags *) |
196 |
218 |
197 fun tagged x = syntax (tag >> PureThy.tag) x; |
219 fun tagged x = syntax (tag >> PureThy.tag) x; |