270 val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " " |
270 val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " " |
271 val parse_value = Scan.repeat1 Parse.xname |
271 val parse_value = Scan.repeat1 Parse.xname |
272 val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) [] |
272 val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) [] |
273 val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) [] |
273 val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) [] |
274 val parse_fact_refs = |
274 val parse_fact_refs = |
275 Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) |
275 Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm) |
276 (Parse.xname -- Scan.option Attrib.thm_sel) |
|
277 >> (fn (name, interval) => |
|
278 Facts.Named ((name, Position.none), interval))) |
|
279 val parse_relevance_chunk = |
276 val parse_relevance_chunk = |
280 (Args.add |-- Args.colon |-- parse_fact_refs >> add_to_relevance_override) |
277 (Args.add |-- Args.colon |-- parse_fact_refs >> add_to_relevance_override) |
281 || (Args.del |-- Args.colon |-- parse_fact_refs |
278 || (Args.del |-- Args.colon |-- parse_fact_refs |
282 >> del_from_relevance_override) |
279 >> del_from_relevance_override) |
283 || (parse_fact_refs >> only_relevance_override) |
280 || (parse_fact_refs >> only_relevance_override) |