equal
deleted
inserted
replaced
1 (* Nominal Function Common |
1 (* Nominal Function Common |
2 Author: Christian Urban |
2 Author: Christian Urban |
|
3 |
|
4 heavily based on the code of Alexander Krauss |
|
5 (code forked on 5 June 2011) |
3 |
6 |
4 Common definitions and other infrastructure for the function package. |
7 Common definitions and other infrastructure for the function package. |
5 *) |
8 *) |
6 |
9 |
7 signature FUNCTION_DATA = |
10 signature FUNCTION_DATA = |
348 || (Parse.reserved "domintros" >> K DomIntros) |
351 || (Parse.reserved "domintros" >> K DomIntros) |
349 || (Parse.reserved "no_partials" >> K No_Partials)) |
352 || (Parse.reserved "no_partials" >> K No_Partials)) |
350 |
353 |
351 fun config_parser default = |
354 fun config_parser default = |
352 (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") []) |
355 (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") []) |
353 >> (fn opts => fold apply_opt opts default) |
356 >> (fn opts => fold Nominal_Function_Common.apply_opt opts default) |
354 in |
357 in |
355 fun function_parser default_cfg = |
358 fun function_parser default_cfg = |
356 config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs |
359 config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs |
357 end |
360 end |
358 |
361 |