Major Section: MISCELLANEOUS
Ld-pre-eval-filter is an
ld special (see ld). The accessor is
(ld-pre-eval-filter state) and the updater is
(set-ld-pre-eval-filter val state).
Ld-pre-eval-filter must be
:query, or a new name that could be defined (e.g., by
defconst). The initial value of
The general-purpose ACL2 read-eval-print loop,
ld, reads forms from
standard-oi, evaluates them and prints the result to
However, there are various flags that control
ld's behavior and
ld-pre-eval-filter is one of them. If the filter is
every form read is evaluated. If the filter is
:query, then after a
form is read it is printed to
standard-co and the user is asked if
the form is to be evaluated or skipped. If the filter is a new
name, then all forms are evaluated until that name is introduced, at
ld terminates normally.
:all filter is, of course, the normal one.
:Query is useful if
you want to replay selected the commands in some file. The new name
filter is used if you wish to replay all the commands in a file up
through the introduction of the given one.