diff options
| -rw-r--r-- | coq/coq.el | 2 | ||||
| -rw-r--r-- | generic/proof-config.el | 3 | ||||
| -rw-r--r-- | generic/proof-shell.el | 2 | ||||
| -rw-r--r-- | lego/lego.el | 2 | ||||
| -rw-r--r-- | plastic/plastic.el | 2 |
5 files changed, 6 insertions, 5 deletions
@@ -81,7 +81,7 @@ (defvar coq-shell-abort-goal-regexp "Current goal aborted" "*Regexp indicating that the current goal has been abandoned.") -(defvar coq-shell-proof-completed-regexp "Subtree proved!" +(defvar coq-shell-proof-completed-regexp "\\(Subtree proved!\\)" "*Regular expression indicating that the proof has been completed.") (defvar coq-goal-regexp 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) diff --git a/lego/lego.el b/lego/lego.el index f7eafdbe..a8b5276e 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -116,7 +116,7 @@ Activates extended printing routines required for Proof General.") "*Regular expression indicating that the proof of the current goal has been abandoned.") -(defvar lego-shell-proof-completed-regexp "\\*\\*\\* QED \\*\\*\\*" +(defvar lego-shell-proof-completed-regexp "\\(\\*\\*\\* QED \\*\\*\\*\\)" "*Regular expression indicating that the proof has been completed.") (defvar lego-save-command-regexp diff --git a/plastic/plastic.el b/plastic/plastic.el index 4ba4586a..14f2b8f3 100644 --- a/plastic/plastic.el +++ b/plastic/plastic.el @@ -144,7 +144,7 @@ "*Regular expression indicating that the proof of the current goal has been abandoned.") -(defvar plastic-shell-proof-completed-regexp "\\*\\*\\* QED \\*\\*\\*" +(defvar plastic-shell-proof-completed-regexp "\\(\\*\\*\\* QED \\*\\*\\*\\)" "*Regular expression indicating that the proof has been completed.") (defvar plastic-save-command-regexp |