equal
deleted
inserted
replaced
479 |
479 |
480 fun mk_rename_decl (aut, (source_aut, rename_f)) = |
480 fun mk_rename_decl (aut, (source_aut, rename_f)) = |
481 add_rename aut source_aut rename_f; |
481 add_rename aut source_aut rename_f; |
482 |
482 |
483 |
483 |
484 (* parsers *) |
484 (* outer syntax *) |
485 |
485 |
486 local structure P = OuterParse and K = OuterKeyword in |
486 local structure P = OuterParse and K = OuterKeyword in |
|
487 |
|
488 val _ = OuterSyntax.keywords ["signature", "actions", "inputs", |
|
489 "outputs", "internals", "states", "initially", "transitions", "pre", |
|
490 "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to", |
|
491 "rename"]; |
487 |
492 |
488 val actionlist = P.list1 P.term; |
493 val actionlist = P.list1 P.term; |
489 val inputslist = P.$$$ "inputs" |-- P.!!! actionlist; |
494 val inputslist = P.$$$ "inputs" |-- P.!!! actionlist; |
490 val outputslist = P.$$$ "outputs" |-- P.!!! actionlist; |
495 val outputslist = P.$$$ "outputs" |-- P.!!! actionlist; |
491 val internalslist = P.$$$ "internals" |-- P.!!! actionlist; |
496 val internalslist = P.$$$ "internals" |-- P.!!! actionlist; |
518 (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |-- |
523 (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |-- |
519 P.!!! (P.name -- (P.$$$ "to" |-- P.list1 P.term))))) >> mk_restriction_decl || |
524 P.!!! (P.name -- (P.$$$ "to" |-- P.list1 P.term))))) >> mk_restriction_decl || |
520 (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term)))))) |
525 (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term)))))) |
521 >> mk_rename_decl; |
526 >> mk_rename_decl; |
522 |
527 |
523 val automatonP = |
528 val _ = |
524 OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl |
529 OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl |
525 (ioa_decl >> Toplevel.theory); |
530 (ioa_decl >> Toplevel.theory); |
526 |
531 |
527 end; |
532 end; |
528 |
533 |
529 |
534 end; |
530 (* setup outer syntax *) |
|
531 |
|
532 val _ = OuterSyntax.add_keywords ["signature", "actions", "inputs", |
|
533 "outputs", "internals", "states", "initially", "transitions", "pre", |
|
534 "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to", |
|
535 "rename"]; |
|
536 |
|
537 val _ = OuterSyntax.add_parsers [automatonP]; |
|
538 |
|
539 |
|
540 end; |
|