equal
deleted
inserted
replaced
53 val add_tyco_syntax: string -> string -> tyco_syntax option -> theory -> theory |
53 val add_tyco_syntax: string -> string -> tyco_syntax option -> theory -> theory |
54 val add_const_syntax: string -> string -> const_syntax option -> theory -> theory |
54 val add_const_syntax: string -> string -> const_syntax option -> theory -> theory |
55 val add_reserved: string -> string -> theory -> theory |
55 val add_reserved: string -> string -> theory -> theory |
56 val add_include: string -> string * (string * string list) option -> theory -> theory |
56 val add_include: string -> string * (string * string list) option -> theory -> theory |
57 |
57 |
58 val codegen_tool: string (*theory name*) -> bool -> string (*export_code expr*) -> unit |
58 val codegen_tool: string (*theory name*) -> string (*export_code expr*) -> unit |
59 end; |
59 end; |
60 |
60 |
61 structure Code_Target : CODE_TARGET = |
61 structure Code_Target : CODE_TARGET = |
62 struct |
62 struct |
63 |
63 |
690 end; (*local*) |
690 end; (*local*) |
691 |
691 |
692 |
692 |
693 (** external entrance point -- for codegen tool **) |
693 (** external entrance point -- for codegen tool **) |
694 |
694 |
695 fun codegen_tool thyname qnd cmd_expr = |
695 fun codegen_tool thyname cmd_expr = |
696 let |
696 let |
697 val thy = Thy_Info.get_theory thyname; |
697 val thy = Thy_Info.get_theory thyname; |
698 val _ = quick_and_dirty := qnd; |
|
699 val parse = Scan.read Token.stopper (Parse.!!! code_exprP) o |
698 val parse = Scan.read Token.stopper (Parse.!!! code_exprP) o |
700 (filter Token.is_proper o Outer_Syntax.scan Position.none); |
699 (filter Token.is_proper o Outer_Syntax.scan Position.none); |
701 in case parse cmd_expr |
700 in case parse cmd_expr |
702 of SOME f => (writeln "Now generating code..."; f thy) |
701 of SOME f => (writeln "Now generating code..."; f thy) |
703 | NONE => error ("Bad directive " ^ quote cmd_expr) |
702 | NONE => error ("Bad directive " ^ quote cmd_expr) |