| author | haftmann |
| Fri, 23 Feb 2007 08:39:19 +0100 | |
| changeset 22346 | 6a4203148945 |
| parent 21884 | 7df02627898e |
| child 24220 | a479ac416ac2 |
| 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@21884 | 16 |
echo "Usage: $PRG IMAGE THY SERI" |
| haftmann@21884 | 17 |
echo |
| haftmann@21884 | 18 |
echo " Issues code generation using image IMAGE," |
| haftmann@21884 | 19 |
echo " theory THY," |
| haftmann@21884 | 20 |
echo " with Isar command 'code_gen SERI'" |
| 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@21884 | 32 |
SERI="$1" |
| haftmann@21884 | 33 |
|
| haftmann@21884 | 34 |
|
| haftmann@21884 | 35 |
## main |
| haftmann@21884 | 36 |
|
| haftmann@21884 | 37 |
SERI=$(echo $SERI | sed -e 's/\\/\\\\"/g; s/"/\\\"/g') |
| haftmann@21884 | 38 |
CMD="Isar.toplevel (fn _ => (use_thy \"$THY\"; CodegenPackage.codegen_command (theory \"$THY\") \"$SERI\"))" |
| haftmann@21884 | 39 |
|
| haftmann@21884 | 40 |
"$ISABELLE" -q -e "$CMD" "$IMAGE" |