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


ProofGeneral-devel mailing list

Reply via email to