		Search-engine friendly clone of the ACL2 documentation.

Output-controls

Set-inhibit-output-lst

Control output

Examples:
(set-inhibit-output-lst '(warning))
(set-inhibit-output-lst '(proof-tree prove proof-builder))
(set-inhibit-output-lst *valid-output-names*) ; inhibit all prover output
:set-inhibit-output-lst (proof-tree prove)

General Form:
(set-inhibit-output-lst x)

where x 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 (but for hard errors, see below)
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-builder  commentary produced by the interactive proof-builder
event          non-proof commentary produced by events such as defun
               and encapsulate
history        output from history commands such as :ubt and :pbt
summary        the summary at the successful conclusion of an event
proof-tree     proof-tree output
comment        output from cw, cw!, and utilities like time$ that use them

It is possible to inhibit each kind of output by putting the corresponding name into x. For example, if 'warning is included in (the value of) x, 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.

Note that proof output can be controlled without inhibiting it using this utility, and indeed is already quite limited by default. See set-gag-mode.

See with-output for a variant of this utility that can be used in books. Also see set-inhibit-warnings and set-inhibit-er for how to inhibit individual warning and error output types, respectively, and see set-inhibited-summary-types for how to inhibit individual parts of the summary.

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

Normally, hard error messages (see er) are not inhibited. To inhibit those as well when ERROR output is inhibited: (assign inhibit-er-hard t). To restore the original behavior: (assign inhibit-er-hard nil).

To get the current of names representing kinds of inhibit output, evaluate (@ inhibit-output-lst).

Note for advanced users. By including warning! in the value of the input, you are automatically including warning as well: all warnings will be inhibited. This is not the case if you modify value of state global variable 'inhibit-output-lst directly (with assign or f-put-global); then, if you include warning! but not warning, then warnings not related to soundness will still be printed (which is probably not what was intended).