Move utility span-make-modifying-removing-span to span.el

1 files changed, 1 insertions, 8 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 63d185ed..19cebe9c 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -722,7 +722,7 @@ Argument FACE means add 'face property FACE to the span."
 		       (goto-char (span-end span))
 		       (skip-chars-backward " \n\t")
 		       (point)))
-	 (newspan     (span-make newstart newend)))
+	 (newspan     (span-make-modifying-removing-span newstart newend)))
     
     (span-set-property span 'pg-helpspan newspan) ; link from parent
 
@@ -745,8 +745,6 @@ Argument FACE means add '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)))
@@ -755,11 +753,6 @@ Argument FACE means add 'face property FACE to the span."
 	(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)))
-
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;