ld prints the forms to be eval'd
Major Section: MISCELLANEOUS
Ld-pre-eval-print is an ld special (see ld). The accessor is
(ld-pre-eval-print state) and the updater is
(set-ld-pre-eval-print val state). Ld-pre-eval-print must be
either t, nil, or :never. The initial value of ld-pre-eval-print 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-pre-eval-print is one of them. If this global variable is t,
then before evaluating the form just read from standard-oi, ld
prints the form to standard-co. If the variable is nil, no such
printing occurs. The t option is useful if you are reading from a
file of commands and wish to assemble a complete script of the
session in standard-co.
The value :never of ld-pre-eval-print is rarely used. During
the evaluation of encapsulate and of certify-book forms,
subsidiary events are normally printed, even if ld-pre-eval-print
is nil. Thus for example, when the user submits an
encapsulate form, all subsidiary events are generally printed
even in the default situation where ld-pre-eval-print is nil.
But occasionally one may want to suppress such printing. In that
case, ld-pre-eval-print should be set to :never.
