diff -r ad436fa9fc5b -r 64fdbee67135 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Thu Sep 23 09:53:52 2010 +0200 +++ b/src/Tools/Code/code_target.ML Thu Sep 23 10:37:28 2010 +0200 @@ -28,8 +28,6 @@ val check_code: theory -> string list -> ((string * bool) * Token.T list) list -> unit - val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit - type serializer type literals = Code_Printer.literals val add_target: string * { serializer: serializer, literals: literals, @@ -56,6 +54,8 @@ val add_const_syntax: string -> string -> const_syntax option -> theory -> theory val add_reserved: string -> string -> theory -> theory val add_include: string -> string * (string * string list) option -> theory -> theory + + val codegen_tool: string (*theory name*) -> bool -> string (*export_code expr*) -> unit end; structure Code_Target : CODE_TARGET = @@ -683,13 +683,20 @@ Outer_Syntax.command "export_code" "generate executable code for constants" Keyword.diag (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of))); -fun shell_command thyname cmd = Toplevel.program (fn _ => - (use_thy thyname; case Scan.read Token.stopper (Parse.!!! code_exprP) - ((filter Token.is_proper o Outer_Syntax.scan Position.none) cmd) - of SOME f => (writeln "Now generating code..."; f (Thy_Info.get_theory thyname)) - | NONE => error ("Bad directive " ^ quote cmd))) - handle Runtime.TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure; - end; (*local*) + +(** external entrance point -- for codegen tool **) + +fun codegen_tool thyname qnd cmd_expr = + let + val thy = Thy_Info.get_theory thyname; + val _ = quick_and_dirty := qnd; + val parse = Scan.read Token.stopper (Parse.!!! code_exprP) o + (filter Token.is_proper o Outer_Syntax.scan Position.none); + in case parse cmd_expr + of SOME f => (writeln "Now generating code..."; f thy) + | NONE => error ("Bad directive " ^ quote cmd_expr) + end; + end; (*struct*)