		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-jclasses+jcmembers

Pretty-print a class declaration or class member declaration.

These are mutually recursive because classes may be class members.

Definitions and Theorems

Function: print-jcmember

(defun print-jcmember (member indent-level)
  (declare (xargs :guard (and (jcmemberp member)
                              (natp indent-level))))
  (let ((__function__ 'print-jcmember))
    (declare (ignorable __function__))
    (jcmember-case
         member
         :field (list (print-jfield member.get indent-level))
         :method (print-jmethod member.get indent-level)
         :class (print-jclass member.get indent-level))))

Function: print-jcbody-element

(defun print-jcbody-element (body-element indent-level)
 (declare (xargs :guard (and (jcbody-element-p body-element)
                             (natp indent-level))))
 (let ((__function__ 'print-jcbody-element))
   (declare (ignorable __function__))
   (jcbody-element-case
        body-element
        :member (print-jcmember body-element.get indent-level)
        :init (print-jcinitializer body-element.get indent-level))))

Function: print-jcbody-element-list

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

Function: print-jclass

(defun print-jclass (class indent-level)
 (declare (xargs :guard (and (jclassp class)
                             (natp indent-level))))
 (let ((__function__ 'print-jclass))
  (declare (ignorable __function__))
  (b* (((jclass class) class)
       (modifiers (msg "~@0~@1~@2~@3~@4"
                       (print-jaccess class.access)
                       (if class.abstract? "abstract " "")
                       (if class.static? "static " "")
                       (if class.final? "final " "")
                       (if class.strictfp? "strictfp " ""))))
   (append
    (list
     (print-jline
      (msg
        "~@0class ~@1 ~@2{" modifiers class.name
        (if class.superclass? (msg "extends ~@0 " class.superclass?)
          ""))
      indent-level))
    (print-jcbody-element-list class.body (1+ indent-level))
    (list (print-jline "}" indent-level))))))

Theorem: return-type-of-print-jcmember.lines

(defthm return-type-of-print-jcmember.lines
  (b* ((?lines (print-jcmember member indent-level)))
    (msg-listp lines))
  :rule-classes :rewrite)

Theorem: return-type-of-print-jcbody-element.lines

(defthm return-type-of-print-jcbody-element.lines
  (b* ((?lines (print-jcbody-element body-element indent-level)))
    (msg-listp lines))
  :rule-classes :rewrite)

Theorem: return-type-of-print-jcbody-element-list.lines

(defthm return-type-of-print-jcbody-element-list.lines
  (b*
   ((?lines (print-jcbody-element-list body-elements indent-level)))
   (msg-listp lines))
  :rule-classes :rewrite)

Theorem: return-type-of-print-jclass.lines

(defthm return-type-of-print-jclass.lines
  (b* ((?lines (print-jclass class indent-level)))
    (msg-listp lines))
  :rule-classes :rewrite)

Subtopics

Print-jcbody-element-list: Pretty-print a sequence of class body declarations.
Print-jcmember: Pretty-print a class member declaration.
Print-jcbody-element: Pretty-print a class body declaration.
Print-jclass: Pretty-print a class declaration.