# HG changeset patch
# User haftmann
# Date 1285231048 -7200
# Node ID 64fdbee6713541dfaf79527baa488ea705c23e67
# Parent  ad436fa9fc5b0576628f364d29f7ff436c14c198
improved and tuned external codegen tool

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*)
diff -r ad436fa9fc5b -r 64fdbee67135 src/Tools/Code/lib/Tools/codegen
--- a/src/Tools/Code/lib/Tools/codegen	Thu Sep 23 09:53:52 2010 +0200
+++ b/src/Tools/Code/lib/Tools/codegen	Thu Sep 23 10:37:28 2010 +0200
@@ -10,27 +10,28 @@
 function usage()
 {
   echo
-  echo "Usage: isabelle $PRG [OPTIONS] IMAGE THY CMD"
+  echo "Usage: isabelle $PRG [OPTIONS] IMAGE THYNAME CMD"
   echo
   echo "  Options are:"
   echo "    -q    run in quick'n'dirty mode"
   echo
   echo "  Issues code generation using image IMAGE,"
-  echo "  theory THY,"
+  echo "  theory THYNAME,"
   echo "  with Isar command 'export_code CMD'"
   echo
   exit 1
 }
 
+
 ## process command line
 
-QUICK_AND_DIRTY=0
+QUICK_AND_DIRTY="false"
 
 while getopts "q" OPT
 do
   case "$OPT" in
     q)
-      QUICK_AND_DIRTY=1
+      QUICK_AND_DIRTY="true"
       ;;
     \?)
       usage
@@ -43,23 +44,20 @@
 [ "$#" -ne 3 ] && usage
 
 IMAGE="$1"; shift
-THY="$1"; shift
-CMD="$1"
+THYNAME="$1"; shift
+CODE_EXPR=$(echo "$1" | perl -pe 's/\\/\\\\/g; s/"/\\\"/g')
 
 
-## main
+## invoke code generation
 
-CODE_CMD=$(echo $CMD | perl -pe 's/\\/\\\\/g; s/"/\\\"/g')
+FORMAL_CMD="Toplevel.program (fn () => ML_Context.eval_text_in \
+  (SOME (ProofContext.init_global (Thy_Info.get_theory thyname))) false Position.none ml_cmd) \
+  handle _ => OS.Process.exit OS.Process.failure;"
 
-if [ "$QUICK_AND_DIRTY" -eq 1 ]
-then
-  QND_FLAG="true"
-else
-  QND_FLAG="false"
-fi
+ACTUAL_CMD="val thyname = \"$THYNAME\"; \
+  val qnd = $QUICK_AND_DIRTY; \
+  val cmd_expr = \"$CODE_EXPR\"; \
+  val ml_cmd = \"Code_Target.codegen_tool thyname qnd cmd_expr\"; \
+  $FORMAL_CMD"
 
-CTXT_CMD="ML_Context.eval_text_in (SOME (ProofContext.init_global (Thy_Info.get_theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
-
-FULL_CMD="quick_and_dirty := $QND_FLAG; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
-
-"$ISABELLE_PROCESS" -q -e "$FULL_CMD" "$IMAGE" || exit 1
+"$ISABELLE_PROCESS" -r -q -e "$ACTUAL_CMD" "$IMAGE" || exit 1