#!/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
THY=$(echo $THY | sed -e 's/\\/\\\\"/g; s/"/\\\"/g')
ISAR="theory Codegen imports \"$THY\" begin export_code $CMD end"
echo "$ISAR" | "$ISABELLE_TOOL" tty -l "$IMAGE" || exit 1