From 16622cef5d14f0b994707bff45362da06eb50f79 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 18 Jul 2002 20:36:53 +0000
Subject: Fix bug in proof-zap-commas-region (which is anyway faulty)

---
 generic/proof-syntax.el | 23 ++++++++++++-----------
 1 file changed, 12 insertions(+), 11 deletions(-)

diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index 34dc13f2..eb873b45 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -152,17 +152,18 @@ Default is comma separated, or SEPREGEXP if set."
   "Remove the face of all `,' within the region (START,END).
 The optional argument LENGTH has no effect. It is required so that we
 may assign this function to `after-change-function'."
-  (save-excursion
-    (let 
-	((start (progn (goto-char start) (beginning-of-line) (point)))
-	 (end (progn (goto-char end) (end-of-line) (point))))
-      (goto-char start)
-      (while (search-forward "," end t)
-	(if (memq (get-char-property (- (point) 1) 'face)
-		(list 'proof-declaration-name-face
-		  'font-lock-function-name-face))
-	    (font-lock-unfontify-region (- (point) 1) (point))
-	    )))))
+  (save-match-data
+    (save-excursion
+      (let 
+	  ((start (progn (goto-char start) (beginning-of-line) (point)))
+	   (end (progn (goto-char end) (end-of-line) (point))))
+	(goto-char start)
+	(while (search-forward "," end t)
+	  (if (memq (get-char-property (- (point) 1) 'face)
+		    (list 'proof-declaration-name-face
+			  'font-lock-function-name-face))
+	      (font-lock-unfontify-region (- (point) 1) (point))
+	    ))))))
 
 (defun proof-zap-commas-buffer () 
   "Remove the face of all `,' in the current buffer."
-- 
cgit v1.2.3