diff options
| -rw-r--r-- | generic/proof-script.el | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 1a8d7c11..8f30ec44 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -688,6 +688,8 @@ Argument FACE means add regular face property FACE to the span." ;; " for menu)"))) )) (span-set-property newspan 'keymap pg-span-context-menu-keymap) + (span-set-property newspan 'modification-hooks + (list 'pg-delete-self-modification-hook)) (if (or (facep mouseface) (setq mouseface (unless mouseface 'proof-mouse-highlight-face))) @@ -695,8 +697,11 @@ Argument FACE means add regular face property FACE to the span." (if face (span-set-property newspan 'face face)) (span-set-property newspan 'priority 50))) - +(defun pg-delete-self-modification-hook (span &rest args) + "Hook for overlay modification-hooks, which deletes SPAN." + (if (span-live-p span) + (span-delete span))) |