equal
deleted
inserted
replaced
11 PRG="$(basename "$0")" |
11 PRG="$(basename "$0")" |
12 |
12 |
13 function usage() |
13 function usage() |
14 { |
14 { |
15 echo |
15 echo |
16 echo "Usage: $PRG IMAGE THY SERI" |
16 echo "Usage: $PRG IMAGE THY CMD" |
17 echo |
17 echo |
18 echo " Issues code generation using image IMAGE," |
18 echo " Issues code generation using image IMAGE," |
19 echo " theory THY," |
19 echo " theory THY," |
20 echo " with Isar command 'export_code SERI'" |
20 echo " with Isar command 'export_code CMD'" |
21 echo |
21 echo |
22 exit 1 |
22 exit 1 |
23 } |
23 } |
24 |
24 |
25 |
25 |
27 |
27 |
28 [ "$#" -lt 2 -o "$1" = "-?" ] && usage |
28 [ "$#" -lt 2 -o "$1" = "-?" ] && usage |
29 |
29 |
30 IMAGE="$1"; shift |
30 IMAGE="$1"; shift |
31 THY="$1"; shift |
31 THY="$1"; shift |
32 SERI="$1" |
32 CMD="$1" |
33 |
33 |
34 |
34 |
35 ## main |
35 ## main |
36 |
36 |
37 SERI=$(echo $SERI | sed -e 's/\\/\\\\"/g; s/"/\\\"/g') |
37 CMD=$(echo $CMD | sed -e 's/\\/\\\\"/g; s/"/\\\"/g') |
38 CMD="Isar.toplevel (fn _ => (use_thy \"$THY\"; CodePackage.codegen_command (theory \"$THY\") \"$SERI\"));" |
38 FULL_CMD="CodePackage.codegen_shell_command \"$THY\" \"$CMD\";" |
39 |
39 |
40 "$ISABELLE" -q -e "$CMD" "$IMAGE" |
40 "$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1 |