389 (*************************************************************************) |
389 (*************************************************************************) |
390 (******************************** Parsers ********************************) |
390 (******************************** Parsers ********************************) |
391 (*************************************************************************) |
391 (*************************************************************************) |
392 |
392 |
393 val opt_thm_name' : (bool * Attrib.binding) parser = |
393 val opt_thm_name' : (bool * Attrib.binding) parser = |
394 Parse.$$$ "(" -- Parse.$$$ "unchecked" -- Parse.$$$ ")" >> K (true, Attrib.empty_binding) |
394 @{keyword "("} -- @{keyword "unchecked"} -- @{keyword ")"} >> K (true, Attrib.empty_binding) |
395 || Parse_Spec.opt_thm_name ":" >> pair false |
395 || Parse_Spec.opt_thm_name ":" >> pair false |
396 |
396 |
397 val spec' : (bool * (Attrib.binding * string)) parser = |
397 val spec' : (bool * (Attrib.binding * string)) parser = |
398 opt_thm_name' -- Parse.prop >> (fn ((a, b), c) => (a, (b, c))) |
398 opt_thm_name' -- Parse.prop >> (fn ((a, b), c) => (a, (b, c))) |
399 |
399 |
400 val alt_specs' : (bool * (Attrib.binding * string)) list parser = |
400 val alt_specs' : (bool * (Attrib.binding * string)) list parser = |
401 let val unexpected = Scan.ahead (Parse.name || Parse.$$$ "[" || Parse.$$$ "(") |
401 let val unexpected = Scan.ahead (Parse.name || @{keyword "["} || @{keyword "("}) |
402 in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! (Parse.$$$ "|"))) end |
402 in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! (@{keyword "|"}))) end |
403 |
403 |
404 val _ = |
404 val _ = |
405 Outer_Syntax.local_theory "fixrec" "define recursive functions (HOLCF)" Keyword.thy_decl |
405 Outer_Syntax.local_theory "fixrec" "define recursive functions (HOLCF)" Keyword.thy_decl |
406 (Parse.fixes -- (Parse.where_ |-- Parse.!!! alt_specs') |
406 (Parse.fixes -- (Parse.where_ |-- Parse.!!! alt_specs') |
407 >> (fn (fixes, specs) => add_fixrec_cmd fixes specs)) |
407 >> (fn (fixes, specs) => add_fixrec_cmd fixes specs)) |