From 3dafa92b1296c494106f0e68ae28c722ce5031df Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Mon, 14 Sep 2009 23:21:33 +0000 Subject: Surpress warnings for dynamic scoping --- coq/coq.el | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/coq/coq.el b/coq/coq.el index 14d3b4f6..94e30d65 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -976,10 +976,11 @@ Currently this doesn't take the loadpath into account." ;; Pre-processing of input string (PG 3.5) ;; -;; Remark: `action' and `string' are known by `proof-shell-insert-hook' -(defun coq-preprocessing () ;; NB: dynamic scoping of `string' +;; Remark: `action' and `string' are known by `proof-shell-insert-hook' +(defun coq-preprocessing () (if coq-time-commands - (setq string (concat "Time " string)))) + (with-no-warnings ;; NB: dynamic scoping of `string' + (setq string (concat "Time " string))))) (add-hook 'proof-shell-insert-hook 'coq-preprocessing) @@ -1107,8 +1108,8 @@ Based on idea mentioned in Coq reference manual." (defun coq-insert-infoH-hook () - (setq string (concat "infoH " string)) - ) + (with-no-warnings ;; NB: dynamic scoping of `string' + (setq string (concat "infoH " string)))) ;; da: FIXME untested with new generic hybrid code: hope this still works (defun coq-insert-as () @@ -1306,12 +1307,13 @@ buffer." "Internal variable. Do not use as configuration variable.") ;; if a command is sent to coq without being in the script, then don't -;; higilight the error.  Remark: `action' and `string' are known by +;; higilight the error. Remark: `action' and `string' are known by ;; `proof-shell-insert-hook', but not by ;; `proof-shell-handle-error-or-interrupt-hook' (defun coq-decide-highlight-error () (setq coq-allow-highlight-error - (not (eq action 'proof-done-invisible)))) + (not (with-no-warnings ;; Dynamic scope of `action' + (eq action 'proof-done-invisible))))) (defun coq-highlight-error-hook () (if coq-allow-highlight-error (coq-highlight-error t t))) -- cgit v1.2.3