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 span-delete-hooks
This approach relies on the fact that spans are deleted when
the corresponding commands are retracted. What is currently
stored in span-delete-action would become a member of
span-delete-hooks. For the spans of Require commands I would
add another function that unlocks ancestors.
2. call a hook in proof-done-retracting
This seems more natural first, because proof-done-retracting
is the right place to unlock ancestors. However, the span
inside proof-done-retracting specifies the region to retract,
the command spans must be computed from it. This is more
complicated and would have to be done on every retract. In
contrast point 1 does not cause any penalty for retracts
without Require commands.
Unless somebody disagrees, I will do point 1.
BTW, what is the relation of 'remove-action and
'span-delete-action? If there is a hook, the remove action could
also be put into the hook.
ProofGeneral-devel mailing list