Error highlighting in coq only when scripting (not when sending

command invisibly).

1 files 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)