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. - D. 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 > buffer? > > I reused an existing test case, see the description in > coq/ex/test-cases/retract-completely-asserted/README. > > I would like to leave the work on the fix to you. > > Hendrik > _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
