		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-jlines-to-channel

Write pretty-printed lines to an output channel.

Signature
(print-jlines-to-channel lines channel state) → state
Arguments: lines — Guard (msg-listp lines).; channel — Guard (symbolp channel).

Definitions and Theorems

Function: print-jlines-to-channel

(defun print-jlines-to-channel (lines channel state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (msg-listp lines)
                              (symbolp channel))))
  (let ((__function__ 'print-jlines-to-channel))
    (declare (ignorable __function__))
    (cond ((endp lines) state)
          (t (b* (((mv & state)
                   (fmt1! "~@0" (list (cons #\0 (car lines)))
                          0 channel state nil)))
               (print-jlines-to-channel (cdr lines)
                                        channel state))))))