636 fold_map (fn x => g |-- f >> pair x) xs |
636 fold_map (fn x => g |-- f >> pair x) xs |
637 :|-- (fn xys => pair ((x, y) :: xys))); |
637 :|-- (fn xys => pair ((x, y) :: xys))); |
638 |
638 |
639 fun process_multi_syntax parse_thing parse_syntax change = |
639 fun process_multi_syntax parse_thing parse_syntax change = |
640 (Parse.and_list1 parse_thing |
640 (Parse.and_list1 parse_thing |
641 :|-- (fn things => Scan.repeat1 (Parse.$$$ "(" |-- Parse.name -- |
641 :|-- (fn things => Scan.repeat1 (@{keyword "("} |-- Parse.name -- |
642 (zip_list things parse_syntax (Parse.$$$ "and")) --| Parse.$$$ ")"))) |
642 (zip_list things parse_syntax (@{keyword "and"})) --| @{keyword ")"}))) |
643 >> (Toplevel.theory oo fold) |
643 >> (Toplevel.theory oo fold) |
644 (fn (target, syns) => fold (fn (raw_x, syn) => change target raw_x syn) syns); |
644 (fn (target, syns) => fold (fn (raw_x, syn) => change target raw_x syn) syns); |
645 |
645 |
646 in |
646 in |
647 |
647 |
665 | NONE => error "Bad serializer arguments"; |
665 | NONE => error "Bad serializer arguments"; |
666 |
666 |
667 |
667 |
668 (** Isar setup **) |
668 (** Isar setup **) |
669 |
669 |
670 val (inK, module_nameK, fileK, checkingK) = ("in", "module_name", "file", "checking"); |
670 val code_expr_argsP = Scan.optional (@{keyword "("} |-- Args.parse --| @{keyword ")"}) []; |
671 |
|
672 val code_expr_argsP = Scan.optional (Parse.$$$ "(" |-- Args.parse --| Parse.$$$ ")") []; |
|
673 |
671 |
674 val code_exprP = |
672 val code_exprP = |
675 Scan.repeat1 Parse.term_group :|-- (fn raw_cs => |
673 Scan.repeat1 Parse.term_group :|-- (fn raw_cs => |
676 ((Parse.$$$ checkingK |-- Scan.repeat (Parse.name |
674 ((@{keyword "checking"} |-- Scan.repeat (Parse.name |
677 -- ((Parse.$$$ "?" |-- Scan.succeed false) || Scan.succeed true) -- code_expr_argsP)) |
675 -- ((@{keyword "?"} |-- Scan.succeed false) || Scan.succeed true) -- code_expr_argsP)) |
678 >> (fn seris => check_code_cmd raw_cs seris) |
676 >> (fn seris => check_code_cmd raw_cs seris) |
679 || Scan.repeat (Parse.$$$ inK |-- Parse.name |
677 || Scan.repeat (@{keyword "in"} |-- Parse.name |
680 -- Scan.optional (Parse.$$$ module_nameK |-- Parse.name) "" |
678 -- Scan.optional (@{keyword "module_name"} |-- Parse.name) "" |
681 -- Scan.optional (Parse.$$$ fileK |-- Parse.name) "" |
679 -- Scan.optional (@{keyword "file"} |-- Parse.name) "" |
682 -- code_expr_argsP) >> (fn seris => export_code_cmd raw_cs seris))); |
680 -- code_expr_argsP) >> (fn seris => export_code_cmd raw_cs seris))); |
683 |
681 |
684 val _ = |
682 val _ = |
685 Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl ( |
683 Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl ( |
686 process_multi_syntax Parse.xname (Scan.option Parse.string) |
684 process_multi_syntax Parse.xname (Scan.option Parse.string) |
687 add_class_syntax_cmd); |
685 add_class_syntax_cmd); |
688 |
686 |
689 val _ = |
687 val _ = |
690 Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl ( |
688 Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl ( |
691 process_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname) |
689 process_multi_syntax (Parse.xname --| @{keyword "::"} -- Parse.xname) |
692 (Scan.option (Parse.minus >> K ())) |
690 (Scan.option (Parse.minus >> K ())) |
693 add_instance_syntax_cmd); |
691 add_instance_syntax_cmd); |
694 |
692 |
695 val _ = |
693 val _ = |
696 Outer_Syntax.command "code_type" "define code syntax for type constructor" Keyword.thy_decl ( |
694 Outer_Syntax.command "code_type" "define code syntax for type constructor" Keyword.thy_decl ( |
711 |
709 |
712 val _ = |
710 val _ = |
713 Outer_Syntax.command "code_include" "declare piece of code to be included in generated code" |
711 Outer_Syntax.command "code_include" "declare piece of code to be included in generated code" |
714 Keyword.thy_decl ( |
712 Keyword.thy_decl ( |
715 Parse.name -- Parse.name -- (Parse.text :|-- (fn "-" => Scan.succeed NONE |
713 Parse.name -- Parse.name -- (Parse.text :|-- (fn "-" => Scan.succeed NONE |
716 | s => Scan.optional (Parse.$$$ "attach" |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME)) |
714 | s => Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME)) |
717 >> (fn ((target, name), content_consts) => |
715 >> (fn ((target, name), content_consts) => |
718 (Toplevel.theory o add_include_cmd target) (name, content_consts)) |
716 (Toplevel.theory o add_include_cmd target) (name, content_consts)) |
719 ); |
717 ); |
720 |
718 |
721 val _ = |
719 val _ = |