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
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
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to