*** empty log message ***

6 files changed, 72 insertions, 65 deletions

diff --git a/af2/af2-fun.el b/af2/af2-fun.el
index 3a5a56f6..ff442fbc 100644
--- a/af2/af2-fun.el
+++ b/af2/af2-fun.el
@@ -26,14 +26,23 @@ send a compile command to af2 for the theorem which name is under the cursor."
 
 (setq
  af2-forget-id-command "del %s.\n"
- af2-sy-definition-regexp "[ \t\n\r]\\(Cst\\|def\\)[ \t\n\r]+\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)" 
- af2-definition-regexp "[ \t\n\r]\\(Cst\\|def\\|claim\\|Sort\\)[ \t\n\r]+\\([^ =\\[]+\\)"
+ af2-comments-regexp "[ \n\t\r]*\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)*"
+ af2-ident-regexp "\\(\\([^ \n\t\r=\\[.]\\|\\(\\.[^ \n\t\r]\\)\\)+\\)"
+ af2-spaces-regexp "[ \n\t\r]*"
+ af2-sy-definition-regexp (concat 
+   "\\(Cst\\|def\\)"
+   af2-comments-regexp
+   "\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)") 
+ af2-definition-regexp (concat
+   "\\(Cst\\|def\\|claim\\|Sort\\)"
+   af2-comments-regexp
+   af2-ident-regexp)
 )
 
 (defun af2-find-and-forget (span)
   (let (str ans tmp (lsp -1))
     (while span 
-      (setq str (proof-remove-comment (span-property span 'cmd)))
+      (setq str (span-property span 'cmd))
 
       (cond
 
@@ -46,11 +55,11 @@ send a compile command to af2 for the theorem which name is under the cursor."
        ((proof-string-match af2-sy-definition-regexp str)
 	(setq ans 
 	      (concat (format af2-forget-id-command 
-				  (concat "$" (match-string 4 str))) ans)))
+				  (concat "$" (match-string 7 str))) ans)))
 
        ((proof-string-match af2-definition-regexp str)
 	(setq ans (concat (format af2-forget-id-command 
-				      (match-string 2 str)) ans))))
+				      (match-string 5 str)) ans))))
 
 
       (setq lsp (span-start span))
diff --git a/af2/af2.el b/af2/af2.el
index 1bb523c7..10dd0573 100644
--- a/af2/af2.el
+++ b/af2/af2.el
@@ -113,8 +113,16 @@
    proof-state-command             "goals."
    proof-goal-command-regexp       "goal\\|prop\\|proposition\\|lem\\|lemma\\|fact\\|cor\\|corollary\\|theo\\|theorem"
    proof-save-command-regexp       "save"
-   proof-goal-with-hole-regexp     "\\(prop\\|proposition\\|lem\\|lemma\\|fact\\|cor\\|corollary\\|theo\\|theorem\\)[ \n\t\r]+\\([^ \n\t\r]+\\)"
-   proof-save-with-hole-regexp     "save[ \n\t\r]+\\(\\([^ \n\t\r]+\\)\\)"
+   proof-goal-with-hole-regexp     (concat 
+      "\\(prop\\|proposition\\|lem\\|lemma\\|fact\\|cor\\|corollary\\|theo\\|theorem\\)"
+      af2-comments-regexp
+      af2-ident-regexp)
+   proof-goal-with-hole-result     5
+   proof-save-with-hole-regexp     (concat 
+      "save"
+      af2-comments-regexp
+      af2-ident-regexp)
+   proof-save-with-hole-result     4
    proof-shell-error-regexp        "^\\([^ \n\t\r]* \\)?\\(e\\|E\\)rror"
    proof-non-undoables-regexp      "undo"
    proof-goal-command              "goal %s."
diff --git a/af2/example.af2 b/af2/example.af2
index 4dc3abb7..36ece411 100644
--- a/af2/example.af2
+++ b/af2/example.af2
@@ -4,6 +4,6 @@
     $Id$
 *)
 
-prop test /\X (X -> X).
+prop (* test *) (* just un test *) test /\X (X -> X).
 trivial.
 save.
\ No newline at end of file
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