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 [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
