David Aspinall <david.aspin...@ed.ac.uk> writes:
So I agree that your approach 1 is best.
Implemented and seems to work, but see my next post on "Reverse
> 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.
ProofGeneral-devel mailing list