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
32
33
34
35
36
37
|
<html>
<head><title>LD-PRE-EVAL-PRINT.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>LD-PRE-EVAL-PRINT</h2>determines whether <code><a href="LD.html">ld</a></code> prints the forms to be <code>eval</code>'d
<pre>Major Section: <a href="MISCELLANEOUS.html">MISCELLANEOUS</a>
</pre><p>
<code>Ld-pre-eval-print</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-print state)</code> and the updater is
<code>(set-ld-pre-eval-print val state)</code>. <code>Ld-pre-eval-print</code> must be
either <code>t</code>, <code>nil</code>, or <code>:never</code>. The initial value of <code>ld-pre-eval-print</code> is
<code>nil</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-print</code> is one of them. If this global variable is <code>t</code>,
then before evaluating the form just read from <code><a href="STANDARD-OI.html">standard-oi</a></code>, <code><a href="LD.html">ld</a></code>
prints the form to <code><a href="STANDARD-CO.html">standard-co</a></code>. If the variable is <code>nil</code>, no such
printing occurs. The <code>t</code> option is useful if you are reading from a
file of <a href="COMMAND.html">command</a>s and wish to assemble a complete script of the
session in <code><a href="STANDARD-CO.html">standard-co</a></code>.<p>
The value <code>:never</code> of <code>ld-pre-eval-print</code> is rarely used. During
the evaluation of <code><a href="ENCAPSULATE.html">encapsulate</a></code> and of <code><a href="CERTIFY-BOOK.html">certify-book</a></code> forms,
subsidiary events are normally printed, even if <code>ld-pre-eval-print</code>
is <code>nil</code>. Thus for example, when the user submits an
<code><a href="ENCAPSULATE.html">encapsulate</a></code> form, all subsidiary events are generally printed
even in the default situation where <code>ld-pre-eval-print</code> is <code>nil</code>.
But occasionally one may want to suppress such printing. In that
case, <code>ld-pre-eval-print</code> should be set to <code>:never</code>. As
described elsewhere (see <a href="SET-INHIBIT-OUTPUT-LST.html">set-inhibit-output-lst</a>), another way to
suppress such printing is to execute <code>(set-inhibit-output-lst lst)</code>
where <code>lst</code> evaluates to a list including <code>'prove</code> and <code>'event</code>.
<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>
|
