Printer
The VL printer is a tool for building strings. It is generally used
to pretty-print our internal Verilog syntax back out into text or HTML.
This is very useful in warnings, the vl-server, and other
contexts.
We implement an applicative ``printer'' for building strings.
Building strings incrementally is difficult in an applicative setting. Our
printer is implemented using a ACL2::stobj named ps. The act of
``printing'' to this stobj essentially just accumulates characters (or strings)
onto a vl-printedlist. The printed elements are kept in reverse order,
which makes it reasonably efficient to successively print small chunks of
text.
Our printer has a variety of configurable features that are useful for
pretty-printing source code, including:
- Support for both text and HTML output
- Automatic column tracking (for, e.g., tab support and line wrapping)
- Automatic word-wrapping of long lines
- A print base for controlling numeric output (e.g., print numbers in hex)
- Other miscellaneous settings
Supporting HTML is subtle because, depending on the context, you may wish to
write:
- HTML markup (e.g., <b>, <code>, ...), where special
characters like < are not to be changed, and where all of the characters
in these tags will be ``invisible'' to the user and should not affect the
current column number.
- Parts of URLs (e.g., filenames), which must be "percent encoded"
per RFC 3986, e.g., space
characters become %20. These, too, do not affect the column number
because they take part only in tags such as <a href="...">.
- Ordinary text, where special characters like & and <
become & and <. Here we also print tabs as a sequence of
characters, and we advance the column number as characters are
printed.
Subtopics
- Ps
- The printer state stobj.
- Verilog-printing
- Printing routines for displaying SystemVerilog constructs.
- Basic-printing
- Primitive routines for printing objects.
- Printing-locally
- How to use ps to build strings in a local context.
- Formatted-printing
- Higher-level routines for printing objects with a fmt- or
cw-like feel.
- Accessing-printed-output
- How to access the characters that have been printed.
- Json-printing
- Routines for encoding various ACL2 structures into JSON format.
- Vl-printedlist
- Backward-compatibility aliases for str::printtree.
