Major Section: IO
General Form: (without-evisc form)where
form is any expression to evaluate. The effect is to evaluate
form as though the without-evisc wrapper were absent, except that
expressions are printed in full for the ensuing output, regardless of the
current evisc-tuples (see set-evisc-tuple). See set-iprint for an example.More precisely, without-evisc binds each of the term-evisc-tuple,
ld-evisc-tuple, abbrev-evisc-tuple and gag-mode-evisc-tuple to
nil (see set-evisc-tuple). It does not modify the trace evisc-tuple, so
trace output is not modified by without-evisc. Also note that calls of
printing functions such as fmt that include explicit evisc-tuples will
not have those evisc-tuples overridden. The following example illustrates
this point.
ACL2 !>(without-evisc
(fms "~x0~%"
(list (cons #0 '((a b ((c d)) e f g) u v w x y)))
*standard-co*
state
(evisc-tuple 2 3 nil nil)))
((A B # ...) U V ...)
<state>
ACL2 !>
We conclude with two remarks. (1) A call of without-evisc on expression
exp actually invokes a specialized call of ld on a one-element list
containing exp, which prints the value returned by evaluation of exp
but actually returns the useless value (mv nil :invisible state). So do
not use without-evisc in programs; just use it at the top level of the
ACL2 read-eval-print loop, or at least the top level of ld. (2) Even
when using without-evisc, if the ACL2 logical world is part of the value
returned, it will be printed in abbreviated form because the ACL2
read-eval-print loop always arranges for this to be the case, regardless of
the ld-evisc-tuple. For example:
ACL2 !>(without-evisc (w state)) <world> ACL2 !>
An alternative to the use of without-evisc is to explore large objects
using the ACL2 function (walkabout object state). Some brief
documentation is printed when you enter an interactive loop upon evaluating a
call of walkabout. We may add documentation for walkabout if that
is requested.
