src/Tools/Code/code_target.ML

     -> string -> int option -> string -> Token.T list -> string * string option list
   val present_code: theory -> string list -> (Code_Thingol.naming -> string list)
     -> string -> int option -> string -> Token.T list -> string
   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,
     check: { env_var: string, make_destination: Path.T -> Path.T,

   val add_instance_syntax: string -> class * string -> unit option -> theory -> theory
   val add_tyco_syntax: string -> string -> tyco_syntax option -> theory -> theory
   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 =
 struct
 

 
 val _ =
   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*)