Higher-level routines for printing objects with a fmt- or
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
- ~&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.
- Basic fmt-like printing function for ps.
- Like vl-basic-cw, but reads its format string from an object.
- Basic cw-like printing function for ps.