diff -r 341cefa2e4da -r 7df02627898e lib/Tools/codegen
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/codegen	Mon Dec 18 08:57:41 2006 +0100
@@ -0,0 +1,41 @@
+#!/usr/bin/env bash
+#
+# $Id$
+# Author: Florian Haftmann, TUM
+#
+# DESCRIPTION: issue code generation from shell
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+  echo
+  echo "Usage: $PRG IMAGE THY SERI"
+  echo
+  echo "  Issues code generation using image IMAGE,"
+  echo "  theory THY,"
+  echo "  with Isar command 'code_gen SERI'"
+  echo
+  exit 1
+}
+
+
+## process command line
+
+[ "$#" -lt 2 -o "$1" = "-?" ] && usage
+
+IMAGE="$1"; shift
+THY="$1"; shift
+SERI="$1"
+
+
+## main
+
+SERI=$(echo $SERI | sed -e 's/\\/\\\\"/g; s/"/\\\"/g')
+CMD="Isar.toplevel (fn _ => (use_thy \"$THY\"; CodegenPackage.codegen_command (theory \"$THY\") \"$SERI\"))"
+
+set -x
+"$ISABELLE" -q -e "$CMD" "$IMAGE"