suppressing or turning on specified output for an event

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