src/Tools/Code/lib/Tools/codegen

QND_FLAG is a shell variable, not a string

#!/usr/bin/env bash
#
# Author: Florian Haftmann, TUM
#
# DESCRIPTION: issue code generation from shell


PRG="$(basename "$0")"

function usage()
{
  echo
  echo "Usage: isabelle $PRG [OPTIONS] IMAGE THY CMD"
  echo
  echo "  Options are:"
  echo "    -q    run in quick'n'dirty mode"
  echo
  echo "  Issues code generation using image IMAGE,"
  echo "  theory THY,"
  echo "  with Isar command 'export_code CMD'"
  echo
  exit 1
}

## process command line

QUICK_AND_DIRTY=0

while getopts "q" OPT
do
  case "$OPT" in
    q)
      QUICK_AND_DIRTY=1
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))

[ "$#" -ne 3 ] && usage

IMAGE="$1"; shift
THY="$1"; shift
CMD="$1"


## main

CODE_CMD=$(echo $CMD | perl -pe 's/\\/\\\\/g; s/"/\\\"/g')

if [ "$QUICK_AND_DIRTY" -eq 1 ]
then
  QND_FLAG="true"
else
  QND_FLAG="false"
fi

CTXT_CMD="ML_Context.eval_text_in (SOME (ProofContext.init_global (Thy_Info.get_theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"

FULL_CMD="quick_and_dirty := $QND_FLAG; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"

"$ISABELLE_PROCESS" -q -e "$FULL_CMD" "$IMAGE" || exit 1