• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
      • Std/strings
        • Pretty-printing
          • Pretty-printing-implementation
            • Missing-functionality
            • Printconfig
              • Printconfig-fix
              • Printconfig-p
              • Make-printconfig
              • Printconfig-equiv
              • Printconfig->print-lowercase
              • Printconfig->hard-right-margin
              • Printconfig->flat-right-margin
              • Printconfig->print-radix
              • Printconfig->print-base
              • Printconfig->home-package
              • Change-printconfig
            • Cons-ppr1
            • Print-escaped-charlist
            • Atom-size
            • Print-escaped-str
            • Obj-size
            • Maybe-merge-flat
            • Ppr
            • Printer-instructions
            • Keyword-param-valuep
            • Print-flat-objs
            • Radix-print-int
            • Print-escaped-atom
            • Print-atom
            • Print-escaped-symbol
            • Radix-print-complex
            • Basic-print-complex
            • Radix-print-rat
            • Spaces1
            • Basic-print-rat
            • Basic-print-nat
            • Basic-print-int
            • Spaces
            • My-needs-slashes
            • Pinstlist->max-width
            • Nat-size
            • Special-term-num
            • Print-column
            • Print-base-fix
            • Int-size
            • Keyword-fix
            • Print-instruction
            • Pinst->width
            • In-home-package-p
            • Eviscerated->guts
            • Evisceratedp
            • Pprdot
          • Eviscerate
          • Pretty
          • Revappend-pretty
          • Pretty-list
        • Printtree
        • Base64
        • Charset-p
        • Strtok!
        • Cases
        • Concatenation
        • Html-encoding
        • Character-kinds
        • Substrings
        • Strtok
        • Equivalences
        • Url-encoding
        • Lines
        • Explode-implode-equalities
        • Ordering
        • Numbers
        • Pad-trim
        • Coercion
        • Std/strings/digit-to-char
        • Substitution
        • Symbols
      • Std/osets
      • Std/io
      • Std/basic
      • Std/system
      • Std/typed-lists
      • Std/bitsets
      • Std/testing
      • Std/typed-alists
      • Std/stobjs
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Pretty-printing-implementation

Printconfig

Options that govern various aspects of pretty-printing, e.g., the margins, numeric base, home package for printing symbols, etc.

This is a product type introduced by fty::defprod.

Fields
flat-right-margin — posp
Soft limit that influences how s-expressions get split up into chunks.
hard-right-margin — posp
Column to use for "hard" line wrapping, where lines are forcibly broken up, usually with backslashes.
print-base — print-base-p
Controls whether numbers will be printed in base 2, 8, 10, or 16.
print-radix — booleanp
When set, printed numbers will include a leading base specifier, #b, #o, or #x for base 2, 8, or 16. Base-10 numbers are printed with a trailing radix point, ., i.e., 123 would print as 123..
home-package — symbolp
Controls which symbols will be printed with package prefixes. Typically this should be set to the pkg-witness for the current package. Symbols from the home package, or that have been imported into the home package, are printed without leading package prefixes.
print-lowercase — booleanp
When set, package and symbol names to be printed in lower case, which may improve readability.

In ACL2's pretty-printer, many of these parameters are part of the state. We pull them out into a configuration object so that we can avoid this dependency.

Subtopics

Printconfig-fix
Fixing function for printconfig structures.
Printconfig-p
Recognizer for printconfig structures.
Make-printconfig
Basic constructor macro for printconfig structures.
Printconfig-equiv
Basic equivalence relation for printconfig structures.
Printconfig->print-lowercase
Get the print-lowercase field from a printconfig.
Printconfig->hard-right-margin
Get the hard-right-margin field from a printconfig.
Printconfig->flat-right-margin
Get the flat-right-margin field from a printconfig.
Printconfig->print-radix
Get the print-radix field from a printconfig.
Printconfig->print-base
Get the print-base field from a printconfig.
Printconfig->home-package
Get the home-package field from a printconfig.
Change-printconfig
Modifying constructor for printconfig structures.