WITH-OUTPUT

suppressing or turning on specified output for an event
Major Section:  SWITCHES-PARAMETERS-AND-MODES

Examples:
(with-output
   :off summary      ; turn off the event summary when evaluating the following:
   :gag-mode :goals  ; use gag-mode, with goal names printed
   (defthm app-assoc (equal (app (app x y) z) (app x (app y z)))))

(with-output ; turn off all output :off :all :gag-mode nil (thm (equal (app (app x y) z) (app x (app y z)))))

(with-output ; same as above, showing all output types :off (error warning warning! observation prove proof-checker event expansion summary proof-tree) :gag-mode nil (thm (equal (app (app x y) z) (app x (app y z)))))

(with-output ; as above, but :stack :push says to save current ; inhibit-output-lst, which can be restored in subsidiary ; with-output call that specifies :stack :pop :stack :push :off :all :gag-mode nil (thm (equal (app (app x y) z) (app x (app y z)))))

General Form: (with-output :key1 val1 ... :keyk valk form)

where each :keyi is either :off, :on, :stack, or :gag-mode and vali is as follows. If :keyi is :off or :on, then vali can be :all, and otherwise is a symbol or non-empty list of symbols representing output types that can be inhibited; see set-inhibit-output-lst. If :keyi is :gag-mode, then :vali is one of the legal values for :set-gag-mode. Otherwise :keyi is :stack, in which case :vali is :push or :pop; for now assume that :stack is not specified (we'll return to it below). The result of evaluating the General Form above is to evaluate form, but in an environment where output occurs as follows. If :on :all is specified, then all output is turned on except as inhibited by :off; else if :off :all is specified, then all output is inhibited except as specified by :on; and otherwise, the currently-inhibited output types are reduced as specified by :on and then extended as specified by :off. But if :gag-mode is specified, then before modifying how output is inhibited, gag-mode is set for the evaluation of form as specified by the value of :gag-mode; see set-gag-mode.

Note: When the scope of with-output is exited, then all modifications are undone, reverting gag-mode and the state of output inhibition to those which were present before the with-output call was entered.

The :stack keyword's effect is illustrated by the following example, where ``(encapsulate nil)'' may replaced by ``(progn'' without any change to the output that is printed.

(with-output
 :stack :push :off :all
 (encapsulate ()
   (defun f1 (x) x)
   (with-output :stack :pop (defun f2 (x) x))
   (defun f3 (x) x)
   (with-output :stack :pop :off warning (in-theory nil))
   (defun f4 (x) x)))
The outer with-output call saves the current output settings (as may have been modified by earlier calls of set-inhibit-output-lst), by pushing them onto a stack, and then turns off all output. Each inner with-output call temporarily pops that stack, restoring the starting output settings, until it completes and undoes the effects of that pop. Unless event output was inhibited at the top level (see set-inhibit-output-lst), the following output is shown:
Since F2 is non-recursive, its admission is trivial.  We observe that
the type of F2 is described by the theorem (EQUAL (F2 X) X).  
And then, if summary output was not inhibited at the top level, we get the rest of this output:
Summary
Form:  ( DEFUN F2 ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Summary Form: ( IN-THEORY NIL) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Note that the use of :off warning supresses a "Theory" warning for the (in-theory nil) event, and that in no case will output be printed for definitions of f1, f3, or f4, or for the encapsulate event itself.

The following more detailed explanation of :stack is intended only for advanced users. After :gag-mode is handled (if present) but before :on or :off is handled, the value of :stack is handled as follows. If the value is :push, then state global inhibit-output-lst-stack is modified by pushing the value of state global inhibit-output-lst onto the value of state global inhibit-output-lst-stack, which is nil at the top level. If the value is :pop, then state global inhibit-output-lst-stack is modified only if non-nil, in which case its top element is popped and becomes the value of of state global inhibit-output-lst.

Warning: With-output has no effect in raw Lisp, and hence is disallowed in function bodies. However, you can probably get the effect you want as illustrated below, where <form> must return an error triple (mv erp val state); see ld.

Examples avoiding with-output, for use in function definitions:

; Inhibit all output: (state-global-let* ((inhibit-output-lst *valid-output-names*)) <form>)

; Inhibit all warning output: (state-global-let* ((inhibit-output-lst (union-eq (f-get-global 'inhibit-output-lst state) '(warning warning!)))) <form>)

Note that with-output is allowed in books. See embedded-event-form.