suppressing or turning on specified output for an event


; Turn off all output during evaluation of the indicated thm form. (with-output :off :all :gag-mode nil (thm (equal (app (app x y) z) (app x (app y z)))))

; Prove the indicated theorem with the event summary turned off and ; using the :goals setting for gag-mode. (with-output :off summary :gag-mode :goals (defthm app-assoc (equal (app (app x y) z) (app x (app y z)))))

; Same effect as just above: (with-output :on summary :summary :all ; equivalently, (header form rules warnings time) :gag-mode :goals (defthm app-assoc (equal (app (app x y) z) (app x (app y z)))))

; Same as just above, but turn off only the indicated parts of the summary. (with-output :on summary :summary (time rules) :gag-mode :goals ; use gag-mode, with goal names printed (defthm app-assoc (equal (app (app x y) z) (app x (app y z)))))

; Same as specifying :off :all, but showing all output types: (with-output :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)))))

; Same as above, but :stack :push says to save the current ; inhibit-output-lst, which can be restored in a subsidiary with-output call ; that specifies :stack :pop. (with-output :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, :summary, 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. If :keyi is :summary, then vali is either :all or a true-list of symbols each of which belongs to the list *summary-types*, i.e., is one of header, form, rules, warnings, time, or value. 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 every output type is turned on except as inhibited by :off; else if :off :all is specified, then every output type 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. If summary is among the output types that are turned on (not inhibited), then if :summary is specified, the only parts of the summary to be printed will be those specified by the value of :summary. The correspondence should be clear, except perhaps that header refers to the line containing only the word Summary, and value refers to the value of the form printed during evaluation of sequences of events as for progn and encapsulate.

Note that the handling of the :stack argument pays no attention to the :summary argument.

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.

 :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:
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.