1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
<html>
<head><title>LD-PRE-EVAL-FILTER.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>LD-PRE-EVAL-FILTER</h2>determines which forms <code><a href="LD.html">ld</a></code> evaluates
<pre>Major Section: <a href="MISCELLANEOUS.html">MISCELLANEOUS</a>
</pre><p>
<code>Ld-pre-eval-filter</code> is an <code><a href="LD.html">ld</a></code> special (see <a href="LD.html">ld</a>). The accessor is
<code>(ld-pre-eval-filter state)</code> and the updater is
<code>(set-ld-pre-eval-filter val state)</code>. <code>Ld-pre-eval-filter</code> must be
either <code>:all</code>, <code>:query</code>, or a new name that could be defined (e.g., by
<code><a href="DEFUN.html">defun</a></code> or <code><a href="DEFCONST.html">defconst</a></code>). The initial value of <code>ld-pre-eval-filter</code> is
<code>:all</code>.
<p>
The general-purpose ACL2 read-eval-print loop, <code><a href="LD.html">ld</a></code>, reads forms from
<code><a href="STANDARD-OI.html">standard-oi</a></code>, evaluates them and prints the result to <code><a href="STANDARD-CO.html">standard-co</a></code>.
However, there are various flags that control <code><a href="LD.html">ld</a></code>'s behavior and
<code>ld-pre-eval-filter</code> is one of them. If the filter is <code>:all</code>, then
every form read is evaluated. If the filter is <code>:query</code>, then after a
form is read it is printed to <code><a href="STANDARD-CO.html">standard-co</a></code> 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
which time <code><a href="LD.html">ld</a></code> terminates normally.<p>
The <code>:all</code> filter is, of course, the normal one. <code>:Query</code> is useful if
you want to replay selected the <a href="COMMAND.html">command</a>s in some file. The new name
filter is used if you wish to replay all the <a href="COMMAND.html">command</a>s in a file up
through the introduction of the given one.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
