*** empty log message ***

3 files changed, 25 insertions, 8 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