equal
deleted
inserted
replaced
31 CMD="$1" |
31 CMD="$1" |
32 |
32 |
33 |
33 |
34 ## main |
34 ## main |
35 |
35 |
36 THY=$(echo $THY | sed -e 's/\\/\\\\"/g; s/"/\\\"/g') |
36 CODE_CMD=$(echo $CMD | perl -pe 's/\\/\\\\/g; s/"/\\\"/g') |
37 ISAR="theory Codegen imports \"$THY\" begin export_code $CMD end" |
37 CTXT_CMD="ML_Context.eval_in (SOME (ProofContext.init (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";" |
|
38 FULL_CMD="val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD" |
38 |
39 |
39 echo "$ISAR" | "$ISABELLE_PROCESS" -I "$IMAGE" |
40 "$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1 |
40 exit ${PIPESTATUS[1]} |
|