David Aspinall <[email protected]> writes: So I agree that your approach 1 is best.
Implemented and seems to work, but see my next post on "Reverse of proof-register-possibly-new-processed-file". > 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. [...] I agree that it looks like these could be combined into a hook, but please be careful with the order of calling if you try that: I suggest to make it a second refactoring step after converting span-delete-action into span-delete-actions. (It may be that we can also address the minor FIXME on line 2140 of proof-script.el here by letting proof-setup-retract-action take a list of functions to append to the hook, and putting on a function to adjust the proof depth counter there, but let's also try that at a later step). There is now span-add-delete-action which adds a function to the 'span-delete-actions property. But it is only used for the action that was previously stored in 'span-delete-action and for coq-unlock-all-ancestors-of-span. I neither touched the remove action nor that FIXME. Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
