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 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.

Bye,

Hendrik
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to