		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-jfield

Pretty-print a field declaration.

Signature
(print-jfield field indent-level) → line
Arguments: field — Guard (jfieldp field).; indent-level — Guard (natp indent-level).
Returns: line — Type (msgp line).

Definitions and Theorems

Function: print-jfield

(defun print-jfield (field indent-level)
 (declare (xargs :guard (and (jfieldp field)
                             (natp indent-level))))
 (let ((__function__ 'print-jfield))
  (declare (ignorable __function__))
  (b* (((jfield field) field))
    (if field.init?
        (print-jline
             (msg "~@0~@1~@2~@3~@4~@5 ~@6 = ~@7;"
                  (print-jaccess field.access)
                  (if field.static? "static " "")
                  (if field.final? "final " "")
                  (if field.transient? "transient " "")
                  (if field.volatile? "volatile " "")
                  (print-jtype field.type)
                  field.name
                  (print-jexpr field.init? (jexpr-rank-expression)))
             indent-level)
      (print-jline (msg "~@0~@1~@2~@3~@4~@5 ~@6;"
                        (print-jaccess field.access)
                        (if field.static? "static " "")
                        (if field.final? "final " "")
                        (if field.transient? "transient " "")
                        (if field.volatile? "volatile " "")
                        (print-jtype field.type)
                        field.name)
                   indent-level)))))

Theorem: msgp-of-print-jfield

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