ld suppresses details when printing
Major Section: MISCELLANEOUS
Ld-evisc-tuple is an ld special (see ld). The accessor is
(ld-evisc-tuple state) and the updater is
(set-ld-evisc-tuple val state). Ld-evisc-tuple must be either
nil or a list of the form
(alist print-level print-length hiding-cars)where
alist is an alist that pairs objects to strings, print-level
and print-length are either nil or non-negative integers, and
hiding-cars is a list of symbols. The initial value of
ld-evisc-tuple is nil.
The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co.
However, there are various flags that control ld's behavior and
ld-evisc-tuple is one of them. Ld may print the forms it is
evaluating and/or the results of evaluation. If the value of
ld-evisc-tuple is a list as shown above, then ld ``eviscerates'' the
objects it prints before printing them. To ``eviscerate'' an object
we replace certain substructures within it by strings which are
printed in their stead. Print-level and print-length, above, are
used as described in CLTL (pp 372) to replace those substructures
deeper than print-level by ``#'' and those longer than print-length
by ``...''. Alist is used to replace any substructure occuring as a
key in alist by the corresponding string. Finally, any consp x
that starts with one of the symbols in hiding-cars is printed as
<hidden>.
The printing of error messages and warnings, as well as certain other output,
uses a different such evisc-tuple, (default-evisc-tuple state). The
advanced user can override this evisc-tuple with the state global
user-default-evisc-tuple. Similarly, some other printing uses yet
another evisc-tuple, (term-evisc-tuple t state), which can be overridden
with state global user-term-evisc-tuple. We may document these
mechanisms more fully if there is sufficient user interest.
