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

 - D.

ProofGeneral-devel mailing list

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Reply via email to