aboutsummaryrefslogtreecommitdiff
path: root/generic
diff options
context:
space:
mode:
authorMakarius Wenzel1999-09-22 17:03:32 +0000
committerMakarius Wenzel1999-09-22 17:03:32 +0000
commit2ea508d10a1004c335d16b76d73b77e09449ef49 (patch)
tree3b09be0e78010ae424dbe8706d0d999840770244 /generic
parent2c011f19bad738e2c0bfa2bc25c4d103bdad29ce (diff)
proof-completed-regexp: match number 1 is response text;
Diffstat (limited to 'generic')
-rw-r--r--generic/proof-config.el3
-rw-r--r--generic/proof-shell.el2
2 files changed, 3 insertions, 2 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el
index c02d23da..1f85a377 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -841,7 +841,8 @@ The engine matches interrupts before errors."
:group 'proof-shell)
(defcustom proof-shell-proof-completed-regexp nil
- "Regexp matching output indicating a finished proof."
+ "Regexp matching output indicating a finished proof.
+Match number 1 should be the response text."
:type 'regexp
:group 'proof-shell)
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index b2231348..7595e3f7 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -874,7 +874,7 @@ assistant."
(proof-clean-buffer proof-goals-buffer)
(setq proof-shell-proof-completed t)
(setq proof-shell-delayed-output
- (cons 'insert (concat "\n" (match-string 0 string)))))
+ (cons 'insert (concat "\n" (match-string 1 string)))))
((proof-shell-string-match-safe proof-shell-start-goals-regexp string)
(setq proof-shell-proof-completed nil)