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

Reply via email to