pg-set-span-helphighlights: add hook to delete help highlight

on any edit (affects error spans and outdated help spans).

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