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
(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).
ProofGeneral-devel mailing list
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.