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

export ISABELLE_LINE_EDITOR=""

echo "$ISAR" | "$ISABELLE_TOOL" tty -l "$IMAGE"

exit ${PIPESTATUS[1]}