--- 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
--- 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