diff options
| author | Christophe Raffalli | 2000-10-26 17:26:52 +0000 |
|---|---|---|
| committer | Christophe Raffalli | 2000-10-26 17:26:52 +0000 |
| commit | 5a1168cefaac1960b781c2e807eb4a88895519e1 (patch) | |
| tree | 9e39edabb6d6f56efdfcce52e36b290f7159c31b | |
| parent | ff408a30ce02e3268736febd5132b03651b0c319 (diff) | |
*** empty log message ***
| -rw-r--r-- | af2/af2-fun.el | 4 | ||||
| -rw-r--r-- | af2/af2.el | 4 | ||||
| -rw-r--r-- | af2/example.af2 | 4 | ||||
| -rw-r--r-- | 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) @@ -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))) |