src/Tools/Code/code_target.ML
changeset 39646 64fdbee67135
parent 39484 505f95975a5a
child 39659 07549694e2f1
     1.1 --- a/src/Tools/Code/code_target.ML	Thu Sep 23 09:53:52 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Thu Sep 23 10:37:28 2010 +0200
     1.3 @@ -28,8 +28,6 @@
     1.4    val check_code: theory -> string list
     1.5      -> ((string * bool) * Token.T list) list -> unit
     1.6  
     1.7 -  val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
     1.8 -
     1.9    type serializer
    1.10    type literals = Code_Printer.literals
    1.11    val add_target: string * { serializer: serializer, literals: literals,
    1.12 @@ -56,6 +54,8 @@
    1.13    val add_const_syntax: string -> string -> const_syntax option -> theory -> theory
    1.14    val add_reserved: string -> string -> theory -> theory
    1.15    val add_include: string -> string * (string * string list) option -> theory -> theory
    1.16 +
    1.17 +  val codegen_tool: string (*theory name*) -> bool -> string (*export_code expr*) -> unit
    1.18  end;
    1.19  
    1.20  structure Code_Target : CODE_TARGET =
    1.21 @@ -683,13 +683,20 @@
    1.22    Outer_Syntax.command "export_code" "generate executable code for constants"
    1.23      Keyword.diag (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
    1.24  
    1.25 -fun shell_command thyname cmd = Toplevel.program (fn _ =>
    1.26 -  (use_thy thyname; case Scan.read Token.stopper (Parse.!!! code_exprP)
    1.27 -    ((filter Token.is_proper o Outer_Syntax.scan Position.none) cmd)
    1.28 -   of SOME f => (writeln "Now generating code..."; f (Thy_Info.get_theory thyname))
    1.29 -    | NONE => error ("Bad directive " ^ quote cmd)))
    1.30 -  handle Runtime.TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
    1.31 -
    1.32  end; (*local*)
    1.33  
    1.34 +
    1.35 +(** external entrance point -- for codegen tool **)
    1.36 +
    1.37 +fun codegen_tool thyname qnd cmd_expr =
    1.38 +  let
    1.39 +    val thy = Thy_Info.get_theory thyname;
    1.40 +    val _ = quick_and_dirty := qnd;
    1.41 +    val parse = Scan.read Token.stopper (Parse.!!! code_exprP) o
    1.42 +      (filter Token.is_proper o Outer_Syntax.scan Position.none);
    1.43 +  in case parse cmd_expr
    1.44 +   of SOME f => (writeln "Now generating code..."; f thy)
    1.45 +    | NONE => error ("Bad directive " ^ quote cmd_expr)
    1.46 +  end;
    1.47 +
    1.48  end; (*struct*)