		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-jline

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

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

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

Definitions and Theorems

Function: print-jline

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

Theorem: msgp-of-print-jline

(defthm msgp-of-print-jline
  (b* ((line (print-jline content indent-level)))
    (msgp line))
  :rule-classes :rewrite)