		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-jclass-list

Pretty-print a sequence of class declarations.

Signature
(print-jclass-list classes indent-level) → lines
Arguments: classes — Guard (jclass-listp classes).; indent-level — Guard (natp indent-level).
Returns: lines — Type (msg-listp lines).

Each one is preceded by a blank line.

Definitions and Theorems

Function: print-jclass-list

(defun print-jclass-list (classes indent-level)
  (declare (xargs :guard (and (jclass-listp classes)
                              (natp indent-level))))
  (let ((__function__ 'print-jclass-list))
    (declare (ignorable __function__))
    (cond ((endp classes) nil)
          (t (append (list (print-jline-blank))
                     (print-jclass (car classes)
                                   indent-level)
                     (print-jclass-list (cdr classes)
                                        indent-level))))))

Theorem: msg-listp-of-print-jclass-list

(defthm msg-listp-of-print-jclass-list
  (b* ((lines (print-jclass-list classes indent-level)))
    (msg-listp lines))
  :rule-classes :rewrite)