| author | wenzelm |
| Sat, 04 Oct 2008 16:19:00 +0200 | |
| changeset 28502 | 6b0e3e4e1891 |
| parent 28142 | cf8da9bbc584 |
| child 28650 | a7ba12e0d3b7 |
| permissions | -rwxr-xr-x |
| haftmann@21884 | 1 |
#!/usr/bin/env bash |
| haftmann@21884 | 2 |
# |
| haftmann@21884 | 3 |
# $Id$ |
| haftmann@21884 | 4 |
# Author: Florian Haftmann, TUM |
| haftmann@21884 | 5 |
# |
| haftmann@21884 | 6 |
# DESCRIPTION: issue code generation from shell |
| haftmann@21884 | 7 |
|
| haftmann@21884 | 8 |
|
| haftmann@21884 | 9 |
## diagnostics |
| haftmann@21884 | 10 |
|
| haftmann@21884 | 11 |
PRG="$(basename "$0")" |
| haftmann@21884 | 12 |
|
| haftmann@21884 | 13 |
function usage() |
| haftmann@21884 | 14 |
{
|
| haftmann@21884 | 15 |
echo |
| haftmann@25611 | 16 |
echo "Usage: $PRG IMAGE THY CMD" |
| haftmann@21884 | 17 |
echo |
| haftmann@21884 | 18 |
echo " Issues code generation using image IMAGE," |
| haftmann@21884 | 19 |
echo " theory THY," |
| haftmann@25611 | 20 |
echo " with Isar command 'export_code CMD'" |
| haftmann@21884 | 21 |
echo |
| haftmann@21884 | 22 |
exit 1 |
| haftmann@21884 | 23 |
} |
| haftmann@21884 | 24 |
|
| haftmann@21884 | 25 |
|
| haftmann@21884 | 26 |
## process command line |
| haftmann@21884 | 27 |
|
| haftmann@21884 | 28 |
[ "$#" -lt 2 -o "$1" = "-?" ] && usage |
| haftmann@21884 | 29 |
|
| haftmann@21884 | 30 |
IMAGE="$1"; shift |
| haftmann@21884 | 31 |
THY="$1"; shift |
| haftmann@25611 | 32 |
CMD="$1" |
| haftmann@21884 | 33 |
|
| haftmann@21884 | 34 |
|
| haftmann@21884 | 35 |
## main |
| haftmann@21884 | 36 |
|
| haftmann@25611 | 37 |
CMD=$(echo $CMD | sed -e 's/\\/\\\\"/g; s/"/\\\"/g') |
| haftmann@28142 | 38 |
FULL_CMD="Code_Target.shell_command \"$THY\" \"$CMD\";" |
| haftmann@21884 | 39 |
|
| wenzelm@28502 | 40 |
"$ISABELLE_PROCESS" -q -e "$FULL_CMD" "$IMAGE" || exit 1 |