I think the natural place to do this is actually in the prover-specific retraction function, coq-find-and-forget.
But this would also require computing the list of spans in the retracted region, which is avoided in the Coq code now by using span properties to store pointers passed back to Coq. So I agree that your approach 1 is best. > 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. The remove-action was a private action for the script management --- I think only used to delete a region of text for the undo with delete function -- note that it is given the span end points as an argument and called after the span is deleted. The delete action is for other stuff called before the span deletion. In particular, the auxiliary spans for decoration, tooltips, etc use the second one to update the internal maps of auxiliary spans. 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). - D. _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
