*** empty log message ***

2 files changed, 40 insertions, 29 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index fe6c07ac..36423c20 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1004,8 +1004,8 @@ the ACS is marked in the current buffer. If CMD does not match any,
       (let (nam gspan next)
 
 	;; Try to set the name of the theorem from the save
-	(setq cmd (proof-remove-comment cmd))
 	(and proof-save-with-hole-regexp
+	     (setq cmd (proof-remove-comment cmd))
 	     (proof-string-match proof-save-with-hole-regexp cmd)
 	     (setq nam (match-string 2 cmd)))
 
@@ -1025,11 +1025,12 @@ the ACS is marked in the current buffer. If CMD does not match any,
 	     "Proof General: script management confused, couldn't find goal span for save.")
 
 	;; If the name isn't set, try to set it from the goal. 
-	(let ((cmdstr (proof-remove-comment (span-property gspan 'cmd))))
 	  (unless nam
 	    (and proof-goal-with-hole-regexp
-		 (proof-string-match proof-goal-with-hole-regexp cmdstr)
-		 (setq nam (match-string 2 cmdstr)))))
+		 (let ((cmdstr 
+			(proof-remove-comment (span-property gspan 'cmd))))
+		   (proof-string-match proof-goal-with-hole-regexp cmdstr)
+		   (setq nam (match-string 2 cmdstr)))))
 
 	;; As a final desparate attempt, set the name to
 	;; proof-unnamed-theorem-name (Coq actually uses a default
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 35f86bf9..e09dea34 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -681,31 +681,41 @@ If RETURNNOPATH is non-nil, return PROGNAME even if we can't find a full path."
   
 (defun proof-remove-comment (str)
   "proof-remove-comment str: return the string str with all comments removed. Nested comments should work."
-  (if str (let 
-	      ((astr "")
-	       (pos 0)
-	       (lpos 0)
-	       (spos -1)
-               (epos -1)
-	       (lvl 0))
-	    (while (or spos epos)
-	      (setq
-	       spos (if (and spos (< spos lpos)) 
-			(string-match proof-comment-start-regexp str lpos) spos)
-	       epos (if (and epos (< epos lpos)) 
-			(string-match proof-comment-end-regexp str lpos) epos))
-	      (if (and spos (or (not epos) (< spos epos)))
-		  (progn
-		    (if (= lvl 0) (setq astr 
-					(concat astr 
-						(substring str pos spos))))
-		    (setq lpos (+ spos 1) lvl (+ lvl 1)))
-		(if (epos) 
-		    (progn
-		      (setq lpos (+ epos 1) lvl (if (> lvl 0) (- lvl 1) 0))
-		      (if (= lvl 0) (setq pos (+ epos 2)))))))
-	    (setq astr (concat astr (substring str pos)))
-	    astr)))
+  (if (and str proof-comment-start-regexp proof-comment-end-regexp) 
+      (let 
+	  ((astr "") ; the result string
+	   (regexp1 (concat "\\(\"\\)\\|\\(" 
+			    proof-comment-start-regexp "\\)\\|\\("
+			   proof-comment-end-regexp "\\)"))
+	   (regexp2 (concat "\\(\"\\)"))
+	   (pos 0)  ; position of the previous match
+	   (mpos 0) ; position of the current match
+	   (lpos 0) ; start of the substring not in a comment and not
+	            ; yet in astr
+	   (lvl 0)  ; number of level of comments
+	   (in-string nil) ; are we in a string
+	   )
+	(while mpos
+	  (setq mpos 
+		(proof-string-match  (if in-string regexp2 regexp1) str pos))
+	  (cond 
+	   ((match-string 1 str)
+	    (setq pos (+ mpos 1) in-string (not in-string)))
+	   ((match-string 2 str)
+	    (progn
+	      (if (= lvl 0) 
+		  (setq astr (concat astr 
+				     (substring str lpos mpos))))
+	      (setq pos (+ mpos 1) lvl (+ lvl 1))))
+	   ((match-string 3 str)		    
+	    (progn
+	      (setq pos (+ mpos 1) lvl (- lvl 1))
+	      (if (< lvl 0) (error "End comment not closing a start comment"))
+	      (if (= lvl 0) 
+		  (setq lpos 
+			(+ mpos (length (match-string 2 str)))))))))
+	(setq astr (concat astr (substring str pos)))
+	astr)))
 
 ;; End of proof-utils.el
 (provide 'proof-utils)
\ No newline at end of file