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