Major Section: SWITCHES-PARAMETERS-AND-MODES
Examples:
; 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 nil
:gag-mode :goals
(defthm app-assoc (equal (app (app x y) z) (app x (app y z)))))
; Turn on 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; form evaluates to an error triple
(see error-triples); 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*. 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.
(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 and see error-triples.
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.
