# HG changeset patch
# User haftmann
# Date 1197526139 -3600
# Node ID c0deb73077322beb9c1fef1e084a02d04abb09f3
# Parent  72e1563aee09868f22249dfa741c946221e8acb6
isatool codegen now returns exit value

diff -r 72e1563aee09 -r c0deb7307732 lib/Tools/codegen
--- a/lib/Tools/codegen	Thu Dec 13 06:51:22 2007 +0100
+++ b/lib/Tools/codegen	Thu Dec 13 07:08:59 2007 +0100
@@ -13,11 +13,11 @@
 function usage()
 {
   echo
-  echo "Usage: $PRG IMAGE THY SERI"
+  echo "Usage: $PRG IMAGE THY CMD"
   echo
   echo "  Issues code generation using image IMAGE,"
   echo "  theory THY,"
-  echo "  with Isar command 'export_code SERI'"
+  echo "  with Isar command 'export_code CMD'"
   echo
   exit 1
 }
@@ -29,12 +29,12 @@
 
 IMAGE="$1"; shift
 THY="$1"; shift
-SERI="$1"
+CMD="$1"
 
 
 ## main
 
-SERI=$(echo $SERI | sed -e 's/\\/\\\\"/g; s/"/\\\"/g')
-CMD="Isar.toplevel (fn _ => (use_thy \"$THY\"; CodePackage.codegen_command (theory \"$THY\") \"$SERI\"));"
+CMD=$(echo $CMD | sed -e 's/\\/\\\\"/g; s/"/\\\"/g')
+FULL_CMD="CodePackage.codegen_shell_command \"$THY\" \"$CMD\";"
 
-"$ISABELLE" -q -e "$CMD" "$IMAGE"
+"$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1
diff -r 72e1563aee09 -r c0deb7307732 src/Tools/code/code_package.ML
--- a/src/Tools/code/code_package.ML	Thu Dec 13 06:51:22 2007 +0100
+++ b/src/Tools/code/code_package.ML	Thu Dec 13 07:08:59 2007 +0100
@@ -17,7 +17,7 @@
     -> term -> 'a;
   val satisfies_ref: (unit -> bool) option ref;
   val satisfies: theory -> term -> string list -> bool;
-  val codegen_command: theory -> string -> unit;
+  val codegen_shell_command: string (*theory name*) -> string (*cg expr*) -> unit;
 end;
 
 structure CodePackage : CODE_PACKAGE =
@@ -265,10 +265,11 @@
   OuterSyntax.command codeK "generate executable code for constants"
     K.diag (P.!!! (code_exprP code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
 
-fun codegen_command thy cmd =
-  case Scan.read OuterLex.stopper (P.!!! (code_exprP code_cmd)) ((filter OuterLex.is_proper o OuterSyntax.scan) cmd)
-   of SOME f => (writeln "Now generating code..."; f thy)
-    | NONE => error ("Bad directive " ^ quote cmd);
+fun codegen_shell_command thyname cmd = Isar.toplevel (fn _ =>
+  (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! (code_exprP code_cmd)) ((filter OuterLex.is_proper o OuterSyntax.scan) cmd)
+   of SOME f => (writeln "Now generating code..."; f (theory thyname))
+    | NONE => error ("Bad directive " ^ quote cmd)))
+  handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
 
 val _ =
   OuterSyntax.improper_command code_thmsK "print system of defining equations for code" OuterKeyword.diag