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)))))where each(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)
: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)Note that the use ofSummary Form: ( IN-THEORY NIL) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
: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.