		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-jmethod

Pretty-print a method declaration.

Signature
(print-jmethod method indent-level) → lines
Arguments: method — Guard (jmethodp method).; indent-level — Guard (natp indent-level).
Returns: lines — Type (msg-listp lines).

Definitions and Theorems

Function: print-jmethod

(defun print-jmethod (method indent-level)
 (declare (xargs :guard (and (jmethodp method)
                             (natp indent-level))))
 (let ((__function__ 'print-jmethod))
  (declare (ignorable __function__))
  (b* (((jmethod method) method)
       (modifiers (msg "~@0~@1~@2~@3~@4~@5~@6"
                       (print-jaccess method.access)
                       (if method.abstract? "abstract " "")
                       (if method.static? "static " "")
                       (if method.final? "final " "")
                       (if method.synchronized? "synchronized "
                         "")
                       (if method.native? "native " "")
                       (if method.strictfp? "strictfp " ""))))
   (append
    (list
     (print-jline
        (msg "~@0~@1 ~@2(~@3) ~@4{"
             modifiers (print-jresult method.result)
             method.name
             (print-comma-sep (print-jparam-list method.params))
             (if method.throws (msg "throws ~@0 "
                                    (print-comma-sep method.throws))
               ""))
        indent-level))
    (print-jblock method.body (1+ indent-level))
    (list (print-jline "}" indent-level))))))

Theorem: msg-listp-of-print-jmethod

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