From 48d90b7f3ff38e197586a80ea4131330be33ec27 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sun, 20 Sep 2009 21:57:09 +0000
Subject: pg-set-span-helphighlights: add hook to delete help highlight on any
 edit (affects error spans and outdated help spans).

---
 generic/proof-script.el | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'generic/proof-script.el')

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)))
 
 
 
-- 
cgit v1.2.3