From 4ff0c15856641bd69e0994319eba89be10726a2d Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 24 Sep 2001 10:23:36 +0000
Subject: Implement Robert Schnecks idea to help Coq display whole of goals
 output.

---
 generic/proof-shell.el | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index b47ed938..c9ea37f7 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -955,9 +955,18 @@ which see."
        ;; Find the last goal string in the output
        (while (string-match proof-shell-start-goals-regexp string start)
 	 (setq start (match-end 0)))
-       ;; Convention: provers with special characters don't include
-       ;; the match in their goals output.  Others do.
-       (unless proof-shell-first-special-char
+       ;; Convention: provers with special characters appearing in
+       ;; proof-start-goals-regexp don't include the match in their 
+       ;; goals output.  Others do.
+       ;; (Improvement to examine proof-start-goals-regexp suggested
+       ;;  for Coq by Robert Schneck because Coq has specials but
+       ;;  doesn't markup goals output specially).
+       (unless (and 
+		proof-shell-first-special-char
+		(not (string-equal 
+		      proof-shell-start-goals-regexp
+		      (proof-shell-strip-special-annotations 
+		       proof-shell-start-goals-regexp))))
 	 (setq start (match-beginning 0)))
        (setq end (if proof-shell-end-goals-regexp
 		     (string-match proof-shell-end-goals-regexp string start)
-- 
cgit v1.2.3