equal
deleted
inserted
replaced
56 QND_CMD="set" |
56 QND_CMD="set" |
57 else |
57 else |
58 QND_CMD="reset" |
58 QND_CMD="reset" |
59 fi |
59 fi |
60 |
60 |
61 CTXT_CMD="ML_Context.eval_text_in (SOME (ProofContext.init_global (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";" |
61 CTXT_CMD="ML_Context.eval_text_in (SOME (ProofContext.init_global (Thy_Info.get_theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";" |
62 |
62 |
63 FULL_CMD="Unsynchronized.$QND_CMD quick_and_dirty; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD" |
63 FULL_CMD="Unsynchronized.$QND_CMD quick_and_dirty; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD" |
64 |
64 |
65 "$ISABELLE_PROCESS" -q -e "$FULL_CMD" "$IMAGE" || exit 1 |
65 "$ISABELLE_PROCESS" -q -e "$FULL_CMD" "$IMAGE" || exit 1 |