I don't see this. Here, coqtop still survives when I kill a
completely asserted active scripting buffer.

OK confirmed, what happens is that the hook functions are not run because the call is in a path in the code where it is assumed that we haven't changed the state of the buffer after all. Previously that could only happen because the user refused to completely process or retract in a partly completed buffer, but now it can happen because you want to sometimes run this function when the buffer is already completely processed or retracted.

proof-script-deactivate scripting is by now quite garbled with the accumulated logic and your new flag which tells it to sometimes ignore the old logic!

Could you try making a separate path/function for your desired behaviour first? Then we can combine back and clean up this function. i.e., duplicate some of the code in the body of proof-deactivate-scripting in a new function.

OK, I do "make test.coq" and then I see some flickering and
finally emacs hangs. What is the proposed way to use the

The hangs seems to be a deadlock in proof-shell-wait that happens with the new way Coq is started with multiple files. I'm not sure why, perhaps because it gets called before the shell has been completely initialised. I removed that line from the tests for now, it works without the wait.

 - D.
ProofGeneral-devel mailing list

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Reply via email to