print output in full
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)))
             (evisc-tuple 2 3 nil nil)))

((A B # ...) U V ...)
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))
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.