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 important: 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? Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
