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
|
<html>
<head><title>STANDARD-OI.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>STANDARD-OI</h2>the standard object input ``channel''
<pre>Major Section: <a href="PROGRAMMING.html">PROGRAMMING</a>
</pre><p>
<code>Standard-oi</code> is an <code><a href="LD.html">ld</a></code> special (see <a href="LD.html">ld</a>). The accessor is
<code>(standard-oi state)</code> and the updater is <code>(set-standard-oi val state)</code>.
<code>Standard-oi</code> must be an open object input channel, a true list of objects,
or a list of objects whose last <code><a href="CDR.html">cdr</a></code> is an open object input channel.
It is from this source that <code><a href="LD.html">ld</a></code> takes the input forms to process. When
<code><a href="LD.html">ld</a></code> is called, if the value specified for <code>standard-oi</code> is a string or
a list of objects whose last <code><a href="CDR.html">cdr</a></code> is a string, then <code><a href="LD.html">ld</a></code> treats the
string as a file name and opens an object input channel from that file, where
the connected book directory (see <a href="CBD.html">cbd</a>) is used to resolve relative
pathnames. The channel opened by <code><a href="LD.html">ld</a></code> is closed by <code><a href="LD.html">ld</a></code> upon
termination.
<p>
``Standard-oi'' stands for ``standard object input.'' The
read-eval-print loop in <code><a href="LD.html">ld</a></code> reads the objects in <code>standard-oi</code> and
treats them as forms to be evaluated. The initial value of
<code>standard-oi</code> is the same as the value of <code><a href="_star_STANDARD-OI_star_.html">*standard-oi*</a></code>
(see <a href="_star_STANDARD-OI_star_.html">*standard-oi*</a>).
<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>
|
