SET-INHIBIT-OUTPUT-LST

control output 
Major Section:  OTHER


Examples:
(set-inhibit-output-lst '(warning))
(set-inhibit-output-lst '(proof-tree prove proof-checker))
:set-inhibit-output-lst (proof-tree prove)


General Form:
(set-inhibit-output-lst lst)
where lst is a form (which may mention state) that evaluates to a list of names, each of which is the name of one of the following ``kinds'' of output produced by ACL2. 
  error          error messages
  warning        warnings other than those related to soundness
  warning!       warnings (of all degrees of importance)
  observation    observations
  prove          commentary produced by the theorem prover
  proof-checker  commentary produced by the proof-checker
  event          non-proof commentary produced by events such as defun
                 and encapsulate
  expansion      commentary produced by make-event expansion
  summary        the summary at the successful conclusion of an event
  proof-tree     proof-tree output
It is possible to inhibit each kind of output by putting the corresponding name into lst. For example, if 'warning is included in (the value of) lst, then no warnings are printed except those related to soundness, e.g., the inclusion of an uncertified book. Note that proof-tree output is affected by set-inhibit-output-lst; see proof-tree.

Printing of events on behalf of certify-book, encapsulate, or defstobj is inhibited when both 'event and 'prove belong to lst. Otherwise, printing of events is controlled by the ld special ld-pre-eval-print.