		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-to-jfile

Write pretty-printed lines to a file.

Signature
(print-to-jfile lines filename state) → state
Arguments: lines — Guard (msg-listp lines).; filename — Guard (stringp filename).

Definitions and Theorems

Function: print-to-jfile

(defun print-to-jfile (lines filename state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (msg-listp lines)
                              (stringp filename))))
  (let ((__function__ 'print-to-jfile))
    (declare (ignorable __function__))
    (b* (((mv channel state)
          (open-output-channel! filename
                                :character state))
         (state (print-jlines-to-channel lines channel state))
         (state (close-output-channel channel state)))
      state)))