--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Code/lib/Tools/codegen Tue Sep 01 16:39:05 2009 +0200
@@ -0,0 +1,40 @@
+#!/usr/bin/env bash
+#
+# Author: Florian Haftmann, TUM
+#
+# DESCRIPTION: issue code generation from shell
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+ echo
+ echo "Usage: isabelle $PRG IMAGE THY CMD"
+ echo
+ echo " Issues code generation using image IMAGE,"
+ echo " theory THY,"
+ echo " with Isar command 'export_code CMD'"
+ echo
+ exit 1
+}
+
+
+## process command line
+
+[ "$#" -lt 2 -o "$1" = "-?" ] && usage
+
+IMAGE="$1"; shift
+THY="$1"; shift
+CMD="$1"
+
+
+## main
+
+CODE_CMD=$(echo $CMD | perl -pe 's/\\/\\\\/g; s/"/\\\"/g')
+CTXT_CMD="ML_Context.eval_in (SOME (ProofContext.init (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
+FULL_CMD="val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
+
+"$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1