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
ProofGeneral-devel@inf.ed.ac.uk
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.

Reply via email to