determines whether ld suppresses details when printing

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.