David Aspinall <david.aspin...@ed.ac.uk> writes:

   Many thanks for the patch!  I hope some users will test it but there
   aren't many on this list, you might like to advertise your web page on
   the Coq mailing list, perhaps?

Sure, I've done that before the ProofGeneral-devel announcement.

   I'll try to take a look myself soon.

It would be really helpful if you could give some advise on the
error reporting problem, which I posted under the subject
"multiple coq files: error reporting".

If you look at the patch there might be two points that are more

1. the defconst proof-no-fully-processed-buffer in
   generic/proof-script and the changes in
   proof-deactivate-scripting for ensuring that even fully
   asserted coq files are completely retracted.

2. The hook proof-shell-extend-queue-hook (defined in
   generic/proof-config) and its call in proof-extend-queue. I
   figured that I only have to call this hook in
   proof-extend-queue. Is this true?

David Aspinall <david.aspin...@ed.ac.uk> writes:

   I hope to release PG 4.1 shortly to coincide with the Isabelle release
   and had hoped your patch would be ready by then, but maybe not.

What do you mean with shortly?


ProofGeneral-devel mailing list

Reply via email to