diff options
| author | David Aspinall | 2009-09-20 21:57:09 +0000 |
|---|---|---|
| committer | David Aspinall | 2009-09-20 21:57:09 +0000 |
| commit | 48d90b7f3ff38e197586a80ea4131330be33ec27 (patch) | |
| tree | a2f6915b47d6aa3d62825533ffb1ee2ea24d614f /generic/proof-script.el | |
| parent | 342d06d05590372ccfecd1076e207ba95b058141 (diff) | |
pg-set-span-helphighlights: add hook to delete help highlight
on any edit (affects error spans and outdated help spans).
Diffstat (limited to 'generic/proof-script.el')
| -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))) |