equal
deleted
inserted
replaced
343 || ((Parse.reserved "default" |-- Parse.term) >> Default) |
343 || ((Parse.reserved "default" |-- Parse.term) >> Default) |
344 || (Parse.reserved "domintros" >> K DomIntros) |
344 || (Parse.reserved "domintros" >> K DomIntros) |
345 || (Parse.reserved "no_partials" >> K No_Partials)) |
345 || (Parse.reserved "no_partials" >> K No_Partials)) |
346 |
346 |
347 fun config_parser default = |
347 fun config_parser default = |
348 (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") []) |
348 (Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 option_parser) --| @{keyword ")"}) []) |
349 >> (fn opts => fold apply_opt opts default) |
349 >> (fn opts => fold apply_opt opts default) |
350 in |
350 in |
351 fun function_parser default_cfg = |
351 fun function_parser default_cfg = |
352 config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs |
352 config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs |
353 end |
353 end |