678 -- Scan.optional (@{keyword "module_name"} |-- Parse.name) "" |
678 -- Scan.optional (@{keyword "module_name"} |-- Parse.name) "" |
679 -- Scan.optional (@{keyword "file"} |-- Parse.name) "" |
679 -- Scan.optional (@{keyword "file"} |-- Parse.name) "" |
680 -- code_expr_argsP) >> (fn seris => export_code_cmd raw_cs seris))); |
680 -- code_expr_argsP) >> (fn seris => export_code_cmd raw_cs seris))); |
681 |
681 |
682 val _ = |
682 val _ = |
683 Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl ( |
683 Outer_Syntax.command @{command_spec "code_class"} "define code syntax for class" |
684 process_multi_syntax Parse.xname (Scan.option Parse.string) |
684 (process_multi_syntax Parse.xname (Scan.option Parse.string) |
685 add_class_syntax_cmd); |
685 add_class_syntax_cmd); |
686 |
686 |
687 val _ = |
687 val _ = |
688 Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl ( |
688 Outer_Syntax.command @{command_spec "code_instance"} "define code syntax for instance" |
689 process_multi_syntax (Parse.xname --| @{keyword "::"} -- Parse.xname) |
689 (process_multi_syntax (Parse.xname --| @{keyword "::"} -- Parse.xname) |
690 (Scan.option (Parse.minus >> K ())) |
690 (Scan.option (Parse.minus >> K ())) |
691 add_instance_syntax_cmd); |
691 add_instance_syntax_cmd); |
692 |
692 |
693 val _ = |
693 val _ = |
694 Outer_Syntax.command "code_type" "define code syntax for type constructor" Keyword.thy_decl ( |
694 Outer_Syntax.command @{command_spec "code_type"} "define code syntax for type constructor" |
695 process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax |
695 (process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax |
696 add_tyco_syntax_cmd); |
696 add_tyco_syntax_cmd); |
697 |
697 |
698 val _ = |
698 val _ = |
699 Outer_Syntax.command "code_const" "define code syntax for constant" Keyword.thy_decl ( |
699 Outer_Syntax.command @{command_spec "code_const"} "define code syntax for constant" |
700 process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax |
700 (process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax |
701 add_const_syntax_cmd); |
701 add_const_syntax_cmd); |
702 |
702 |
703 val _ = |
703 val _ = |
704 Outer_Syntax.command "code_reserved" "declare words as reserved for target language" |
704 Outer_Syntax.command @{command_spec "code_reserved"} |
705 Keyword.thy_decl ( |
705 "declare words as reserved for target language" |
706 Parse.name -- Scan.repeat1 Parse.name |
706 (Parse.name -- Scan.repeat1 Parse.name |
707 >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds) |
707 >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)); |
708 ); |
708 |
709 |
709 val _ = |
710 val _ = |
710 Outer_Syntax.command @{command_spec "code_include"} |
711 Outer_Syntax.command "code_include" "declare piece of code to be included in generated code" |
711 "declare piece of code to be included in generated code" |
712 Keyword.thy_decl ( |
712 (Parse.name -- Parse.name -- (Parse.text :|-- |
713 Parse.name -- Parse.name -- (Parse.text :|-- (fn "-" => Scan.succeed NONE |
713 (fn "-" => Scan.succeed NONE |
714 | s => Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME)) |
714 | s => Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME)) |
715 >> (fn ((target, name), content_consts) => |
715 >> (fn ((target, name), content_consts) => |
716 (Toplevel.theory o add_include_cmd target) (name, content_consts)) |
716 (Toplevel.theory o add_include_cmd target) (name, content_consts))); |
717 ); |
717 |
718 |
718 val _ = |
719 val _ = |
719 Outer_Syntax.command @{command_spec "code_modulename"} "alias module to other name" |
720 Outer_Syntax.command "code_modulename" "alias module to other name" Keyword.thy_decl ( |
720 (Parse.name -- Scan.repeat1 (Parse.name -- Parse.name) |
721 Parse.name -- Scan.repeat1 (Parse.name -- Parse.name) |
721 >> (fn (target, modlnames) => (Toplevel.theory o fold (add_module_alias target)) modlnames)); |
722 >> (fn (target, modlnames) => (Toplevel.theory o fold (add_module_alias target)) modlnames) |
722 |
723 ); |
723 val _ = |
724 |
724 Outer_Syntax.command @{command_spec "code_abort"} |
725 val _ = |
725 "permit constant to be implemented as program abort" |
726 Outer_Syntax.command "code_abort" "permit constant to be implemented as program abort" |
726 (Scan.repeat1 Parse.term_group >> (Toplevel.theory o fold allow_abort_cmd)); |
727 Keyword.thy_decl ( |
727 |
728 Scan.repeat1 Parse.term_group >> (Toplevel.theory o fold allow_abort_cmd) |
728 val _ = |
729 ); |
729 Outer_Syntax.command @{command_spec "export_code"} "generate executable code for constants" |
730 |
730 (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of))); |
731 val _ = |
|
732 Outer_Syntax.command "export_code" "generate executable code for constants" |
|
733 Keyword.diag (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of))); |
|
734 |
731 |
735 end; (*local*) |
732 end; (*local*) |
736 |
733 |
737 |
734 |
738 (** external entrance point -- for codegen tool **) |
735 (** external entrance point -- for codegen tool **) |