From 17e3598c76cb426e96b973fb49c53a4227877383 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 15 Nov 2011 13:50:51 +0000
Subject: Quick stab at support for switching to proof shell when interactive
 support expected, see Trac #430

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

(limited to 'coq')

diff --git a/coq/coq.el b/coq/coq.el
index 164217cd..d8127211 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1166,14 +1166,17 @@ This is specific to `coq-mode'."
    pg-subterm-end-char ?\374            ; not done
    pg-topterm-regexp "\375"
 
-   proof-shell-eager-annotation-start "\376\\|\\[Reinterning\\|Warning:"
+   ;; FIXME: ideally, the eager annotation should just be a single "special" char,
+   ;; this requires changes in Coq.
+   proof-shell-eager-annotation-start 
+   "\376\\|\\[Reinterning\\|Warning:\\|TcDebug "
    proof-shell-eager-annotation-start-length 12
 
    ;; ****** is added at the end of warnings in emacs mode, this is temporary I
    ;;        want xml like tags, and I want them removed before warning display.
    ;; I want the same for errors -> pgip
 
-   proof-shell-eager-annotation-end "\377\\|done\\]\\|\\*\\*\\*\\*\\*\\*" ; done
+   proof-shell-eager-annotation-end "\377\\|done\\]\\|\\*\\*\\*\\*\\*\\*\\|) >" ; done
    proof-shell-annotated-prompt-regexp coq-shell-prompt-pattern
    proof-shell-result-start "\372 Pbp result \373"
    proof-shell-result-end "\372 End Pbp result \373"
-- 
cgit v1.2.3