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