From 40a7b597d4ac26214bd50bf1b0dc19391fd7f1ad Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Mon, 23 Oct 2006 07:46:42 +0000
Subject: Error highlighting in coq only when scripting (not when sending
 command invisibly).

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

diff --git a/coq/coq.el b/coq/coq.el
index f1d1269d..94e770f3 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1478,11 +1478,22 @@ buffer."
           (delete-span sp)
           )))))
 
-(defun coq-highlight-error-hook ()
-  (save-excursion (coq-highlight-error t t)))
 
+(setq coq-allow-highlight-error t)
+
+;; if a command is sent to coq without being in the script, then don't
+;; higilight the error
+(defun coq-decide-highlight-error ()
+  (if (eq action 'proof-done-invisible)
+      (setq coq-allow-highlight-error nil)
+    (setq coq-allow-highlight-error t)))
+
+(defun coq-highlight-error-hook ()
+  (if coq-allow-highlight-error (save-excursion (coq-highlight-error t t))))
 
+;; We need this two hooks to highlight only when scripting
 (add-hook 'proof-shell-handle-error-or-interrupt-hook 'coq-highlight-error-hook t)
+(add-hook 'proof-shell-insert-hook 'coq-decide-highlight-error t)
 
 (provide 'coq)
 
-- 
cgit v1.2.3