lib/Tools/codegen

consider exit status of code generation direcitve

#!/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