From 5a1168cefaac1960b781c2e807eb4a88895519e1 Mon Sep 17 00:00:00 2001
From: Christophe Raffalli
Date: Thu, 26 Oct 2000 17:26:52 +0000
Subject: *** empty log message ***

---
 af2/af2-fun.el         | 4 ++--
 af2/af2.el             | 4 ++--
 af2/example.af2        | 4 +++-
 generic/proof-utils.el | 2 +-
 4 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/af2/af2-fun.el b/af2/af2-fun.el
index 5da642a3..3a5a56f6 100644
--- a/af2/af2-fun.el
+++ b/af2/af2-fun.el
@@ -26,8 +26,8 @@ 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 "\\(Cst\\|def\\|claim\\|Sort\\)[ \t\n\r]+\\([^ =\\[]+\\)"
+ 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]+\\([^ =\\[]+\\)"
 )
 
 (defun af2-find-and-forget (span)
diff --git a/af2/af2.el b/af2/af2.el
index e9924d0e..1bb523c7 100644
--- a/af2/af2.el
+++ b/af2/af2.el
@@ -107,14 +107,14 @@
   "Configure Proof General scripting for Af2."
   (setq
    proof-terminal-char		?\.	; ends every command
-   proof-script-command-end-regexp "[.][ \n\t\r]"
+   proof-script-command-end-regexp "[.]\\([ \t]\\|$\\)"
    proof-comment-start             "(*"
    proof-comment-end               "*)"
    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]+\\)\\)[ \n\t\r]*\.[ \n\t\r]"
+   proof-save-with-hole-regexp     "save[ \n\t\r]+\\(\\([^ \n\t\r]+\\)\\)"
    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 ae08853d..a196a67b 100644
--- a/af2/example.af2
+++ b/af2/example.af2
@@ -4,4 +4,6 @@
     $Id$
 *)
 
-test.
+goal /\X (X -> X).
+trivial.
+save th.
\ No newline at end of file
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 7816bd3f..299bf7db 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -696,7 +696,7 @@ If RETURNNOPATH is non-nil, return PROGNAME even if we can't find a full path."
 			(string-match proof-comment-end-regexp str lpos) epos))
 	      (if (and spos (or (not epos) (< spos epos)))
 		  (progn
-		    (if (= lvl 0) (setq astr 
+		    (if (<= lvl 0) (setq astr 
 					(concat astr 
 						(substring str pos spos))))
 		    (setq lpos (+ spos 1) lvl (+ lvl 1)))
-- 
cgit v1.2.3