changeset 8733 | 3213613a775a |
parent 8438 | b8389b4fca9c |
child 9317 | 7a72952ca068 |
8732:aef229ca5e77 | 8733:3213613a775a |
---|---|
550 (Scan.optional internalslist []) -- |
550 (Scan.optional internalslist []) -- |
551 stateslist -- |
551 stateslist -- |
552 (Scan.optional initial "True") -- |
552 (Scan.optional initial "True") -- |
553 translist))))) >> mk_ioa_decl || |
553 translist))))) >> mk_ioa_decl || |
554 (P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.list1 P.name))) >> mk_composition_decl || |
554 (P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.list1 P.name))) >> mk_composition_decl || |
555 (P.name -- (P.$$$ "=" |-- (P.$$$ "hide" |-- P.list1 P.term -- (P.$$$ "in" |-- P.name)))) |
555 (P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |-- P.list1 P.term -- (P.$$$ "in" |-- P.name)))) |
556 >> mk_hiding_decl || |
556 >> mk_hiding_decl || |
557 (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |-- P.name -- (P.$$$ "to" |-- P.list1 P.term)))) |
557 (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |-- P.name -- (P.$$$ "to" |-- P.list1 P.term)))) |
558 >> mk_restriction_decl || |
558 >> mk_restriction_decl || |
559 (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- P.name -- (P.$$$ "using" |-- P.term)))) |
559 (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- P.name -- (P.$$$ "using" |-- P.term)))) |
560 >> mk_rename_decl; |
560 >> mk_rename_decl; |
568 |
568 |
569 (* setup outer syntax *) |
569 (* setup outer syntax *) |
570 |
570 |
571 val _ = OuterSyntax.add_keywords ["signature", "actions", "inputs", |
571 val _ = OuterSyntax.add_keywords ["signature", "actions", "inputs", |
572 "outputs", "internals", "states", "initially", "transitions", "pre", |
572 "outputs", "internals", "states", "initially", "transitions", "pre", |
573 "post", "transrel", ":=", "compose", "hide", "in", "restrict", "to", |
573 "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to", |
574 "rename", "using"]; |
574 "rename", "using"]; |
575 |
575 |
576 val _ = OuterSyntax.add_parsers [automatonP]; |
576 val _ = OuterSyntax.add_parsers [automatonP]; |
577 |
577 |
578 |
578 |