aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-shell.el
diff options
context:
space:
mode:
authorGravatar Hendrik Tews <hendrik@askra.de>2011-12-07 09:23:09 +0000
committerGravatar Hendrik Tews <hendrik@askra.de>2011-12-07 09:23:09 +0000
commitbc8a80167ad13742d4cf6b6bf794883516429517 (patch)
tree7b94f8d8203ed95343930c773cc01777ddc61509 /generic/proof-shell.el
parent69533109c96e0089d6dbf755f6e87f41af19ac44 (diff)
- protect proof-shell-handle-delayed-output against the case where
proof-shell-end-goals-regexp is defined but does not match - add coq setting for hiding additional subgoals
Diffstat (limited to 'generic/proof-shell.el')
-rw-r--r--generic/proof-shell.el4
1 files changed, 2 insertions, 2 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 6abef30b..a2402013 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1502,9 +1502,9 @@ i.e., 'goals or 'response."
(while (re-search-forward proof-shell-start-goals-regexp end t)
(setq gstart (match-beginning 0))
(setq gend
- (if proof-shell-end-goals-regexp
+ (if (and proof-shell-end-goals-regexp
+ (re-search-forward proof-shell-end-goals-regexp end t))
(progn
- (re-search-forward proof-shell-end-goals-regexp end t)
(setq rstart (match-end 0))
(match-beginning 0))
end)))