--- a/src/Tools/Code/lib/Tools/codegen Wed Sep 01 08:52:49 2010 +0200
+++ b/src/Tools/Code/lib/Tools/codegen Wed Sep 01 09:03:34 2010 +0200
@@ -53,13 +53,13 @@
if [ "$QUICK_AND_DIRTY" -eq 1 ]
then
- QND_CMD="set"
+ QND_FLAG="true"
else
- QND_CMD="reset"
+ QND_FLAG="false"
fi
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\";"
-FULL_CMD="Unsynchronized.$QND_CMD quick_and_dirty; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
+FULL_CMD="quick_and_dirty := QND_FLAG; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
"$ISABELLE_PROCESS" -q -e "$FULL_CMD" "$IMAGE" || exit 1