Formatted-printing
Higher-level routines for printing objects with a fmt- or
cw-like feel.
We implement limited versions of fmt and cw. The
following ACL2-style directives are supported and behave similarly as those
described in ":doc fmt."
- ~~, prints a tilde
- ~%, prints a newline
- ~|, prints a newline if we are not already on column 0
- ~[space], prints a space
- ~[newline], skips subsequent whitespace
- ~xi, pretty-print an object.
- ~si, prints a string verbatim, or acts like ~xi when given any
non-string object.
- ~&i, print a list, separated by commas, with the word "and"
preceeding the final element.
Note: our pretty-printer is currently very lousy. Its output is not nearly
as nice as ACL2's ordinary ~x directives.
Note: although other ACL2-style directives are not yet supported, we may
eventually extend the printer to allow them.
Subtopics
- Vl-basic-fmt
- Basic fmt-like printing function for ps.
- Vl-basic-cw-obj
- Like vl-basic-cw, but reads its format string from an object.
- Vl-basic-cw
- Basic cw-like printing function for ps.
