• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
        • Getting-started
        • Utilities
        • Loader
        • Transforms
        • Lint
        • Mlib
        • Server
        • Kit
        • Printer
          • Ps
          • Basic-printing
            • Vl-println?
            • Vl-print
            • Vl-printable-p
            • Vl-col-after-printing-string
            • Vl-col-after-printing-chars
            • Vl-print-strings-with-commas
            • Vl-string-needs-html-encoding-p
            • Vl-println-markup
            • Vl-print-strings-as-lines
            • Vl-print-url
            • Vl-print-nat
            • Vl-indent
            • Vl-println
            • Vl-print-markup
            • Vl-ps-seq
            • Vl-cw-ps-seq
            • Vl-when-html
            • Vl-ps-span
          • Verilog-printing
          • Printing-locally
          • Formatted-printing
          • Accessing-printed-output
          • Vl-printedlist
          • Json-printing
        • Esim-vl
        • Well-formedness
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Printer

Basic-printing

Primitive routines for printing objects.

Our printer is intended to support both text and html output. Printing HTML is subtle because one may wish to write:

  • HTML markup (e.g., <b>, <code>, ...), wherein the special characters like < are not to be changed, are going to be invisible to the user, and should not affect the column number,
  • Parts of URLs (e.g., filenames), which must be "percent encoded" per RFC 3986, e.g., spaces become %20. These, too, do not affect the column number because they take part only in tags such as <a href="...">, and
  • Encoded HTML text, where special characters like & and < become &amp; and &lt;, and where tabs become a litany of &nbsp; characters, and where the column should be advanced as the text is printed.

Subtopics

Vl-println?
(vl-println? x &key (ps 'ps)) prints text with automatic encoding, and may also inserts a newline if we have gone past the autowrap-col.
Vl-print
(vl-print x) prints text with automatic encoding.
Vl-printable-p
(vl-printable-p x) recognizes strings, character lists, numbers, and ordinary characters.
Vl-col-after-printing-string
Figure out where we'll be after printing a string.
Vl-col-after-printing-chars
Figure out where we'll be after printing some characters.
Vl-print-strings-with-commas
(vl-print-strings-with-commas x indent &key (ps 'ps)) prints the elements of x, a string list, separated by commas.
Vl-string-needs-html-encoding-p
Vl-println-markup
(vl-println-markup x &key (ps 'ps)) prints verbatim text with no encoding, then prints a newline.
Vl-print-strings-as-lines
(vl-print-strings-as-lines x &key (ps 'ps)) prints the elements of x, a string list, on separate lines.
Vl-print-url
(vl-print-url x &key (ps 'ps)) prints text with automatic URL encoding.
Vl-print-nat
(vl-print-nat x) is an optimized version of vl-print for natural numbers.
Vl-indent
(vl-indent n &key (ps 'ps)) indents to column n.
Vl-println
(vl-println x) prints text with automatic encoding, and always adds a newline.
Vl-print-markup
(vl-print-markup x) prints verbatim text with no encoding.
Vl-ps-seq
Macro for issuing a sequence of printer commands.
Vl-cw-ps-seq
Print to standard-out using ps
Vl-when-html
Like vl-ps-seq, but the commands are only executed when HTML mode is enabled.
Vl-ps-span
Like vl-ps-seq, except that in HTML mode the contents are also wrapped in a <span> tag of the given class.