From 875e1aa9cbf134649927da585ff357177ecdc9f8 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 8 Sep 2009 18:45:16 +0000
Subject: Oops: repair hybrid output broken by two window fix! See trac #109.

---
 coq/coq.el | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index 49699607..9ac70098 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -961,9 +961,8 @@ To be used in `proof-shell-classify-output-system-specific'. "
 (defun coq-hybrid-ouput-goals-response (cmd string)
   "Specific function to deal with hybrid response/goal output from coq.
 To be used in `proof-shell-classify-output-system-specific'."
-  ;; match subgoal list anywhere in the ouput
-  ;; then display the message before it, and then do as a normal goal
-  ;; output.
+  ;; match subgoal list anywhere in the ouput then display the message before
+  ;; it, and then do as a normal goal output.
   (proof-shell-string-match-safe "[0-9]+ subgoals?" string)
   (let* ((start (match-beginning 0))
          (prestring (substring string 0 start))
@@ -974,7 +973,7 @@ To be used in `proof-shell-classify-output-system-specific'."
       ;; (proof-shell-classify-output cmd goalstring)
       (pg-goals-display goalstring) ;; this erases response buffer
       ;; da: I added this test: otherwise 2 window mode seems quite broken?!
-      (unless (string-match "[\t\n ]*" prestring) 
+      (unless (string-equal "" prestring)
         (pg-response-display prestring));; this does not erase goals buffer
       ;(proof-shell-handle-delayed-output-hook)
       (setq coq-last-hybrid-pre-string prestring)
-- 
cgit v1.2.3