		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-line

Pretty-print a (non-blank) line of code.

Signature
(pprint-line content level) → line
Arguments: content — Guard (msgp content).; level — Guard (natp level).
Returns: line — Type (msgp line).

The content to print is preceded by indentation according to the current level.

Definitions and Theorems

Function: pprint-line

(defun pprint-line (content level)
  (declare (xargs :guard (and (msgp content) (natp level))))
  (let ((__function__ 'pprint-line))
    (declare (ignorable __function__))
    (msg "~s0~@1~%" (pprint-indent level)
         content)))

Theorem: msgp-of-pprint-line

(defthm msgp-of-pprint-line
  (b* ((line (pprint-line content level)))
    (msgp line))
  :rule-classes :rewrite)