coq: run silently and explicitly Show when necessary #742
Conversation
hendriktews
force-pushed
the
silent
branch
2 times, most recently
from
afc09c7
to
9821415
Compare
This is a step towards fixing ProofGeneral#568. It fixes the cases after Proof, comments and auto, leaving now 3 instead of 6 failing tests in ci/simple-tests/test-goals-present.el.
- update manuals - expect test goals-reset-after-admitted to fail again - expect errors in tests 020_coq-test-definition, 090_coq-test-regression-Fail and 091_coq-test-regression-Fail
- goals should be reset when there are no more goals (does work) - goals should be reset after Qed (does not work)
Extend the goals present tests to additionally check that the response buffer contains some text (i.e., an error message) in those cases where an error is expected.
This commit fixes two more cases of ProofGeneral#568: The goals buffer is updated in case of an error if Coq is inside a proof. Care is taken to keep the error message in the response buffer and to show the response buffer in two-pane mode. The fix works by issuing a Show command as a priority action item from proof-shell-handle-error-or-interrupt-hook, which runs at the end of the error processing. The new action item flag 'keep-response tells the generic machinery to not clear the response buffer and to keep it in two-pane mode.
|
Hi @erikmd , @Matafou , @cpitclaudel , |
|
The approach used in this PR does not work for Search and Check commands. I'll start from scratch in a new PR. |
|
Thanks a lot for working on this @hendriktews ; I don't have anything smart to say on the implementation at this stage but I'm very glad that you're on it :) |
This is a step towards fixing #568. It fixes the cases after Proof, comments and auto, leaving now 3 instead of 6 failing tests in ci/simple-tests/test-goals-present.el.
The first commit here breaks prooftree. More work is needed.