diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1999-11-16 15:54:52 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1999-11-16 15:54:52 +0000 |
| commit | eddec5f5ba72b2cf373d02794208576b818f569d (patch) | |
| tree | 6c77d183a706a9749eaee8867d4471a4e0379fc2 /generic/proof.el | |
| parent | 17c25f594e5853289ae18553709908b6739e35d4 (diff) | |
Docstrings, bug report msg. Added proof-warn-if-unset.
Diffstat (limited to 'generic/proof.el')
| -rw-r--r-- | generic/proof.el | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/generic/proof.el b/generic/proof.el index 6948ea7c..b5f051ed 100644 --- a/generic/proof.el +++ b/generic/proof.el @@ -168,7 +168,7 @@ of the proof (starting from 1).") ;; Handy macros (defmacro proof-with-current-buffer-if-exists (buf &rest body) - "As with-current-buffer if BUF exists, otherwise nothing." + "As with-current-buffer if BUF exists and is live, otherwise nothing." `(if (buffer-live-p ,buf) (with-current-buffer ,buf ,@body))) @@ -343,10 +343,15 @@ Returns new END value." ;; ----------------------------------------------------------------- -;; Display functions +;; Messaging and display functions ;; +(defun proof-warn-if-unset (tag sym) + "Give a warning (with TAG) if symbol SYM is unbound or nil." + (unless (and (boundp sym) (symbol-value sym)) + (warn "Proof General %s: %s is unset." tag (symbol-name sym)))) + ;; FIXME: this function should be combined with ;; proof-shell-maybe-erase-response-buffer. (defun proof-response-buffer-display (str &optional face) @@ -471,7 +476,9 @@ No action if BUF is nil." "Proof General" (list 'proof-general-version 'proof-assistant) nil nil - "[When reporting a bug, please include a small test case for us to repeat it.]"))) + "[When reporting a bug, please include a small test case for us to repeat it. + Please also check that it is not already covered in the BUGS file that came with + the distribution, or http://zermelo.dcs.ed.ac.uk/~proofgen/ProofGeneral/BUGS]"))) |