David Aspinall <[email protected]> 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 issue. And I don't get an error! You don't see the error any more, because we have now double security: - first the buffer is retract because of proof-no-fully-processed-buffer - second coqtop is killed on switching the active scripting buffer 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 in coq.el. 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 b.v 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.) Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
