		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-jcunit

Pretty-print a compilation unit.

Signature
(print-jcunit cunit) → lines
Arguments: cunit — Guard (jcunitp cunit).
Returns: lines — Type (msg-listp lines).

This function does not have an indentation level argument, because it starts at level 0.

If there is a package declaration, we precede the import declarations (if any) with a blank line to separate the latter from the former.

Definitions and Theorems

Function: print-jcunit

(defun print-jcunit (cunit)
 (declare (xargs :guard (jcunitp cunit)))
 (let ((__function__ 'print-jcunit))
   (declare (ignorable __function__))
   (b* (((jcunit cunit) cunit))
     (append
          (if cunit.package?
              (list (print-jline (msg "package ~@0;" cunit.package?)
                                 0))
            nil)
          (if (and cunit.imports cunit.package?)
              (cons (print-jline-blank)
                    (print-jimports cunit.imports 0))
            (print-jimports cunit.imports 0))
          (print-jclass-list cunit.types 0)))))

Theorem: msg-listp-of-print-jcunit

(defthm msg-listp-of-print-jcunit
  (b* ((lines (print-jcunit cunit)))
    (msg-listp lines))
  :rule-classes :rewrite)