I've committed a patch to proof-protected-process-or-retract now which fixes
this problem and I think your test case works.
But there may be some further issues (try the coq autotest script) because the
coq process is killed and restarted at unusual places in the code now, probably
breaking some assumptions.
I don't quite understand the places where this happens: it would seem cleanest
if the process was started/exited with the activate/deactivate action, but I'm
seeing it being started after switching buffers and beginning scripting
somewhere else, e.g. on the first non-comment element of the file.
On 21 Jan 2011, at 10:06, Hendrik Tews wrote:
> David Aspinall writes:
> Do you want to repair by adding a test for fully processed
> I reused an existing test case, see the description in
> I would like to leave the work on the fix to you.
ProofGeneral-devel mailing list
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.