| author | haftmann |
| Tue, 01 Sep 2009 16:39:05 +0200 | |
| changeset 32481 | 236fa33784de |
| parent 30492 | lib/Tools/codegen@c150e6fa4e0d |
| child 32482 | 522f04b719c8 |
| permissions | -rwxr-xr-x |
| haftmann@21884 | 1 |
#!/usr/bin/env bash |
| haftmann@21884 | 2 |
# |
| haftmann@21884 | 3 |
# Author: Florian Haftmann, TUM |
| haftmann@21884 | 4 |
# |
| haftmann@21884 | 5 |
# DESCRIPTION: issue code generation from shell |
| haftmann@21884 | 6 |
|
| haftmann@21884 | 7 |
|
| haftmann@21884 | 8 |
## diagnostics |
| haftmann@21884 | 9 |
|
| haftmann@21884 | 10 |
PRG="$(basename "$0")" |
| haftmann@21884 | 11 |
|
| haftmann@21884 | 12 |
function usage() |
| haftmann@21884 | 13 |
{
|
| haftmann@21884 | 14 |
echo |
| wenzelm@28650 | 15 |
echo "Usage: isabelle $PRG IMAGE THY CMD" |
| haftmann@21884 | 16 |
echo |
| haftmann@21884 | 17 |
echo " Issues code generation using image IMAGE," |
| haftmann@21884 | 18 |
echo " theory THY," |
| haftmann@25611 | 19 |
echo " with Isar command 'export_code CMD'" |
| haftmann@21884 | 20 |
echo |
| haftmann@21884 | 21 |
exit 1 |
| haftmann@21884 | 22 |
} |
| haftmann@21884 | 23 |
|
| haftmann@21884 | 24 |
|
| haftmann@21884 | 25 |
## process command line |
| haftmann@21884 | 26 |
|
| haftmann@21884 | 27 |
[ "$#" -lt 2 -o "$1" = "-?" ] && usage |
| haftmann@21884 | 28 |
|
| haftmann@21884 | 29 |
IMAGE="$1"; shift |
| haftmann@21884 | 30 |
THY="$1"; shift |
| haftmann@25611 | 31 |
CMD="$1" |
| haftmann@21884 | 32 |
|
| haftmann@21884 | 33 |
|
| haftmann@21884 | 34 |
## main |
| haftmann@21884 | 35 |
|
| haftmann@30492 | 36 |
CODE_CMD=$(echo $CMD | perl -pe 's/\\/\\\\/g; s/"/\\\"/g') |
| haftmann@30492 | 37 |
CTXT_CMD="ML_Context.eval_in (SOME (ProofContext.init (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";" |
| haftmann@30492 | 38 |
FULL_CMD="val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD" |
| haftmann@21884 | 39 |
|
| haftmann@30492 | 40 |
"$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1 |