• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
        • Defun
        • Declare
        • System-utilities
        • Stobj
        • State
        • Mutual-recursion
        • Memoize
        • Mbe
        • Io
        • Defpkg
        • Apply$
        • Loop$
        • Programming-with-state
        • Arrays
        • Characters
        • Time$
        • Defmacro
        • Loop$-primer
        • Fast-alists
        • Defconst
        • Evaluation
        • Guard
        • Equality-variants
        • Compilation
        • Hons
        • ACL2-built-ins
        • Developers-guide
        • System-attachments
        • Advanced-features
        • Set-check-invariant-risk
        • Numbers
        • Efficiency
        • Irrelevant-formals
        • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
        • Redefining-programs
        • Lists
        • Invariant-risk
        • Errors
        • Defabbrev
        • Conses
        • Alists
        • Set-register-invariant-risk
        • Strings
          • 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
          • String-listp
          • Stringp
          • Length
          • Search
          • Remove-duplicates
          • Position
          • Coerce
          • Concatenate
          • Reverse
          • String
          • Subseq
          • Substitute
          • String-upcase
          • String-downcase
          • Count
          • Char
          • String<
          • String-equal
          • String-utilities
          • String-append
          • String>=
          • String<=
          • String>
          • Hex-digit-char-theorems
          • String-downcase-gen
          • String-upcase-gen
        • Program-wrapper
        • Get-internal-time
        • Basics
        • Packages
        • Oracle-eval
        • Defmacro-untouchable
        • <<
        • Primitive
        • Revert-world
        • Unmemoize
        • Set-duplicate-keys-action
        • Symbols
        • Def-list-constructor
        • Easy-simplify-term
        • Defiteration
        • Fake-oracle-eval
        • Defopen
        • Sleep
      • Operational-semantics
      • Real
      • Start-here
      • Debugging
      • Miscellaneous
      • Output-controls
      • Macros
      • Interfacing-tools
    • 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.