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
|
<html>
<head><title>_star_TERMINAL-MARKUP-TABLE_star_.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>*TERMINAL-MARKUP-TABLE*</h2>a <a href="MARKUP.html">markup</a> table used for printing to the terminal
<pre>Major Section: <a href="DOCUMENTATION.html">DOCUMENTATION</a>
</pre><p>
The value of the ACL2 constant <code>*terminal-markup-table*</code> is an association
list pairing <a href="MARKUP.html">markup</a> keys with strings, to be used for printing to the
terminal. See <a href="MARKUP.html">markup</a> for a description of the ACL2 <a href="MARKUP.html">markup</a> language.
<p>
The entries in <code>*terminal-markup-table*</code> are of the form
<pre>
(key . fmt-string)
</pre>
where <code>key</code> is one of the <a href="DOC-STRING.html">doc-string</a> tilde directives
(see <a href="MARKUP.html">markup</a>), and <code>fmt-string</code> is a string as expected by the
ACL2 printing function <code><a href="FMT.html">fmt</a></code>. The system arranges that for any
<code>arg</code>, when an expression ~key[arg] is encountered by the
<a href="DOCUMENTATION.html">documentation</a> printer, <code><a href="FMT.html">fmt</a></code> will print <code>fmt-string</code> in the
association list where <code>#\a</code> is bound to <code>arg</code> and <code>#\A</code> is
bound to the result of applying the function <code><a href="STRING-UPCASE.html">string-upcase</a></code> to
<code>arg</code>.<p>
It is possible to implement tools in ACL2 for printing <a href="DOCUMENTATION.html">documentation</a>
to other than the terminal. In fact, such tools exist for Texinfo
and for HTML. For now, discussion of this capability is beyond the
scope of the present topic.
<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>
|
