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
Hi,
for coq I lock ancestor buffers inside the processing of Require
commands. Because these Require commands may stand at arbitrary
positions in the sources, I should unlock ancestors when Require
commands are retracted. I found the following solutions:
1. convert span-delete-action into
