*** empty log message ***

3 files changed, 47 insertions, 57 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 1c7b75f7..176cb84e 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -921,7 +921,9 @@ NB: This setting is not used for matching output from the prover."
 
 (defcustom proof-save-with-hole-regexp nil 
   "Regexp which matches a command to save a named theorem.
-Match number 2 should be the name of the theorem saved.
+The name of the theorem is build from the variable
+proof-save-with-hole-result using the same convention as 
+query-replace-regexp. 
 Used for setting names of goal..save regions and for default
 function-menu configuration in proof-script-find-next-entity.
 
@@ -929,6 +931,16 @@ It's safe to leave this setting as nil."
   :type 'regexp
   :group 'proof-script)
 
+(defcustom proof-save-with-hole-result 2 
+  "String or Int: how to build the theorem name after matching
+with proof-save-with-hole-regexp. If it is an int N use match-string 
+to recover the value of the Nth parenthesis matched. If it is a string
+use replace-match. It the later case, proof-save-with-hole-regexp should
+match the entire command"
+
+  :type '(choice string int)
+  :group 'proof-script)
+
 ;; FIXME: unify uses so that proof-anchor-regexp works sensibly
 (defcustom proof-goal-command-regexp nil
   "Matches a goal command in the proof script.   
@@ -941,7 +953,9 @@ for `proof-script-next-entity-regexps' used for function menus."
 
 (defcustom proof-goal-with-hole-regexp nil 
   "Regexp which matches a command used to issue and name a goal.
-Match number 2 should be the name of the goal issued.
+The name of the theorem is build from the variable
+proof-goal-with-hole-result using the same convention as 
+query-replace-regexp. 
 Used for setting names of goal..save regions and for default
 function-menu configuration in proof-script-find-next-entity.
 
@@ -949,6 +963,16 @@ It's safe to leave this setting as nil."
   :type 'regexp
   :group 'proof-script)
 
+(defcustom proof-goal-with-hole-result 2
+  "String or Int: how to build the theorem name after matching
+with proof-goal-with-hole-regexp. If it is an int N use match-string 
+to recover the value of the Nth parenthesis matched. If it is a string
+use replace-match. It the later case, proof-goal-with-hole-regexp should
+match the entire command"
+
+  :type '(choice string int)
+  :group 'proof-script)
+
 (defcustom proof-non-undoables-regexp nil
   "Regular expression matching commands which are *not* undoable.
 Used in default functions `proof-generic-state-preserving-p' 
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 36423c20..fa1f4d0e 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1004,11 +1004,15 @@ 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
+	(message 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)))
-
+	     (setq nam 
+		   (if (stringp proof-save-with-hole-result)
+		       (replace-match proof-save-with-hole-result nil nil cmd)
+		     (match-string proof-save-with-hole-result cmd))))
+	(message nam)
 	;; Search backwards for first goal command, 
 	;; deleting spans along the way.
 	(setq gspan span)
@@ -1026,12 +1030,15 @@ the ACS is marked in the current buffer. If CMD does not match any,
 
 	;; If the name isn't set, try to set it from the goal. 
 	  (unless nam
-	    (and proof-goal-with-hole-regexp
-		 (let ((cmdstr 
-			(proof-remove-comment (span-property gspan 'cmd))))
+	    (let ((cmdstr (span-property gspan 'cmd)))
+	      (message cmdstr)
+	      (and proof-goal-with-hole-regexp
 		   (proof-string-match proof-goal-with-hole-regexp cmdstr)
-		   (setq nam (match-string 2 cmdstr)))))
-
+		   (setq nam 
+			 (if (stringp proof-goal-with-hole-result)
+			     (replace-match proof-goal-with-hole-result nil nil cmdstr)
+			   (match-string proof-goal-with-hole-result cmdstr))))))
+	  
 	;; As a final desparate attempt, set the name to
 	;; proof-unnamed-theorem-name (Coq actually uses a default
 	;; name for unnamed theorems, believe it or not, and issues
@@ -1157,10 +1164,14 @@ the ACS is marked in the current buffer. If CMD does not match any,
 
 	  ;; Try to set a name from the goal
 	  ;; (useless for provers like Isabelle)
-	  (let ((cmdstr (proof-remove-comment (span-property gspan 'cmd))))
+	  (let ((cmdstr (span-property gspan 'cmd)))
+	    (message cmdstr)
 	    (and proof-goal-with-hole-regexp
 		 (proof-string-match proof-goal-with-hole-regexp cmdstr)
-	       (setq nam (match-string 2 cmdstr))))
+		 (setq nam 
+		       (if (stringp proof-goal-with-hole-result)
+			   (replace-match proof-goal-with-hole-result nil nil cmdstr)
+			 (match-string proof-goal-with-hole-result cmdstr)))))
 
 	  ;; As a final desparate attempt, set the name to "Unnamed_thm".
 	  (unless nam
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index e09dea34..942acd42 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -672,50 +672,5 @@ If RETURNNOPATH is non-nil, return PROGNAME even if we can't find a full path."
 (setq autoload-package-name "proof")
 (setq generated-autoload-file "proof-autoloads.el")
 	
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; The following function removes comments from a string. Nested 
-;; comments should work. Warning the length of the resulting 
-;; string is reduced, it may be better to replace comments by
-;; white spaces
-  
-(defun proof-remove-comment (str)
-  "proof-remove-comment str: return the string str with all comments removed. Nested comments should work."
-  (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