WITH-OUTPUT

suppressing or turning on specified output for an event 
Major Section:  EVENTS


Example:
(with-output
   :off summary ; turn off the event summary when evaluating the following:
   (in-theory (disable name)))


General Form:
(with-output :key1 val1 ... :keyk valk form)
where each :keyi is either :off or :on and either vali is either :all or else a symbol or non-empty list of symbols representing output types that can be inhibited (see set-inhibit-output-lst). The result of evaluating the General Form above is to evaluate form, but in an environment where the current set of inhibited output types is modified: if :on :all is specified, then all output is turned on except as specified 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.

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>)