		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-jcinitializer

Pretty-print a class initializer.

Signature
(print-jcinitializer initializer indent-level) → lines
Arguments: initializer — Guard (jcinitializerp initializer).; indent-level — Guard (natp indent-level).
Returns: lines — Type (msg-listp lines).

Definitions and Theorems

Function: print-jcinitializer

(defun print-jcinitializer (initializer indent-level)
  (declare (xargs :guard (and (jcinitializerp initializer)
                              (natp indent-level))))
  (let ((__function__ 'print-jcinitializer))
    (declare (ignorable __function__))
    (append
         (list (print-jline (if (jcinitializer->static? initializer)
                                "static {"
                              "{")
                            indent-level))
         (print-jblock (jcinitializer->code initializer)
                       (1+ indent-level))
         (list (print-jline "}" indent-level)))))

Theorem: msg-listp-of-print-jcinitializer

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