equal
deleted
inserted
replaced
394 | params => |
394 | params => |
395 params |> map string_for_raw_param |
395 params |> map string_for_raw_param |
396 |> sort_strings |> cat_lines)) |
396 |> sort_strings |> cat_lines)) |
397 end)) |
397 end)) |
398 |
398 |
399 val parse_query_bang = Parse.$$$ "?" || Parse.$$$ "!" || Parse.$$$ "!!" |
399 val parse_query_bang = @{keyword "?"} || @{keyword "!"} || @{keyword "!!"} |
400 val parse_key = |
400 val parse_key = |
401 Scan.repeat1 (Parse.typ_group || parse_query_bang) >> implode_param |
401 Scan.repeat1 (Parse.typ_group || parse_query_bang) >> implode_param |
402 val parse_value = |
402 val parse_value = |
403 Scan.repeat1 (Parse.xname || Parse.float_number || parse_query_bang) |
403 Scan.repeat1 (Parse.xname || Parse.float_number || parse_query_bang) |
404 val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) [] |
404 val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) [] |
405 val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) [] |
405 val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) [] |
406 val parse_fact_refs = |
406 val parse_fact_refs = |
407 Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm) |
407 Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm) |
408 val parse_relevance_chunk = |
408 val parse_relevance_chunk = |
409 (Args.add |-- Args.colon |-- parse_fact_refs >> add_relevance_override) |
409 (Args.add |-- Args.colon |-- parse_fact_refs >> add_relevance_override) |