Ld-pre-eval-print
Determines whether ld prints the forms to be eval'd
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. Note that the ACL2 top-level loop (see lp) results from
an invocation of ld.
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. As described elsewhere (see set-inhibit-output-lst), another way to suppress such printing is to execute
(set-inhibit-output-lst lst) where lst evaluates to a list including
'prove and 'event.
