		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Print-escaped-atom

Print any arbitrary atom with suitable escaping, obeying the print-base, print-radix, print-lowercase, and home package settings.

Signature
(print-escaped-atom x config acc) → new-acc
Arguments: x — Guard (atom x).; config — Guard (printconfig-p config).
Returns: new-acc — Type (character-listp new-acc), given (character-listp acc).

Definitions and Theorems

Function: print-escaped-atom

(defun print-escaped-atom (x config acc)
  (declare (xargs :guard (and (atom x) (printconfig-p config))))
  (let ((acl2::__function__ 'print-escaped-atom))
    (declare (ignorable acl2::__function__))
    (b* (((when (symbolp x))
          (print-escaped-symbol x config acc))
         ((when (characterp x))
          (b* ((acc (list* #\\ #\# acc)))
            (case x
              (#\Newline (revappend-chars "Newline" acc))
              (#\Space (revappend-chars "Space" acc))
              (#\Page (revappend-chars "Page" acc))
              (#\Tab (revappend-chars "Tab" acc))
              (#\Rubout (revappend-chars "Rubout" acc))
              (#\Return (revappend-chars "Return" acc))
              (otherwise (cons x acc)))))
         ((when (stringp x))
          (b* ((acc (cons #\" acc))
               (acc (print-escaped-str x #\" acc)))
            (cons #\" acc))))
      (print-atom-aux x config acc))))

Theorem: character-listp-of-print-escaped-atom

(defthm character-listp-of-print-escaped-atom
  (implies (character-listp acc)
           (b* ((new-acc (print-escaped-atom x config acc)))
             (character-listp new-acc)))
  :rule-classes :rewrite)