Malformed token: error msg;
scan: explicit handling of malformed symbols from previous stage;
source: interactive flag indicates intermittent error_msg;
tuned;
#!/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\"))"
"$ISABELLE" -q -e "$CMD" "$IMAGE"