David Aspinall <david.aspin...@ed.ac.uk> writes:
OK, I committed a patch now (not quite the one I sent you off list)
which ensures that the hook function is run.
Thanks, we can now close the killing-fully-asserted-active-buffer
And I don't get an error!
You don't see the error any more, because we have now double
- first the buffer is retract because of
- second coqtop is killed on switching the active scripting
At the moment proof-no-fully-processed-buffer is therefore not
necessary, because killing coqtop retracts everything. Eventually
I want coqtop to survive switching the active buffer if the load
path' of the new and old buffer are equal. Then
proof-no-fully-processed-buffer will again be essential.
I just updated the description in that README file, if you want
to see the error you have to disable a deactivate-scripting-hook
Regarding test case above: the bug mentioned in README is fixed, but
the behaviour I described earlier (about Coq process being started at
odd time) still happens when I follow the "To provoke an error"
When do you see coq being restarted? When I follow the old
instructions (that is without disabling the
deactivate-scripting-hook), I see:
- coq starting when I script the first comment in a.v
- coq killed when I script the first comment in b.v
- coq started again when I script the first non-comment line in
This is precisely as it should be. (Only that I don't understand
why I can script the first comment in b.v without coq running.)
ProofGeneral-devel mailing list