From c868833b20cc3c8e3962e5a18a952c84e6c47284 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Tue, 16 Dec 2014 13:07:13 +0000 Subject: Added a way to print eager message without warning face. It is the only way I found to display informativemessage appearing *before* the goal. --- coq/coq.el | 26 +++++++++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) diff --git a/coq/coq.el b/coq/coq.el index e7cf5129..89b5f6ad 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -339,6 +339,31 @@ SMIE is a navigation and indentation framework available in Emacs >= 23.3." ;; Auxiliary code for Coq modes ;; +;; Due to the architecture of proofgeneral, informative message put *before* +;; the goal disappear unless marked as "urgent", i.e. being enclosed with +;; "eager-annotation" syntax. Since we don't want the Warning color to be used +;; for simple informative message, we have to redefine this function to use +;; normal face when the "eager annotation" is acutally not a warning. This is a +;; modified version of the same function in generic/proof-shell.el. +(defun proof-shell-process-urgent-message-default (start end) + "A subroutine of `proof-shell-process-urgent-message'." + ;; Clear the response buffer this time, but not next, leave window. + (pg-response-maybe-erase nil nil) + (proof-minibuffer-message + (buffer-substring-no-properties + (save-excursion + (re-search-forward proof-shell-eager-annotation-start end nil) + (point)) + (min end + (save-excursion (end-of-line) (point)) + (+ start 75)))) + (let ((face + (progn (goto-char start) + (if (looking-at "") 'default-face + 'proof-eager-annotation-face)))) + (pg-response-display-with-face + (proof-shell-strip-eager-annotations start end) + face))) ;;;;;;;;;;; Trying to accept { and } as terminator for empty commands. Actually @@ -1456,7 +1481,6 @@ Warning: (proof-shell-config-done)) - (proof-eval-when-ready-for-assistant (easy-menu-define proof-goals-mode-aux-menu proof-goals-mode-map -- cgit v1.2.3