		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprinted-lines-to-file

Write pretty-printed lines to a file.

Signature
(pprinted-lines-to-file lines filepath state) → (mv erp val state)
Arguments: lines — Guard (msg-listp lines).; filepath — Guard (stringp filepath).

We set the soft and hard right margins to very large values to avoid line breaks in virtually all cases. Setting these margins to ``infinity'' is not supported.

In the future, we may improve the pretty-printer to take into consideration a specified right margin, breaking and identing lines appropriately.

Definitions and Theorems

Function: pprinted-lines-to-file

(defun pprinted-lines-to-file (lines filepath state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (msg-listp lines)
                             (stringp filepath))))
 (let ((__function__ 'pprinted-lines-to-file))
   (declare (ignorable __function__))
   (state-global-let*
        ((fmt-soft-right-margin 1000000 set-fmt-soft-right-margin)
         (fmt-hard-right-margin 1000000 set-fmt-hard-right-margin))
        (b* (((mv channel state)
              (open-output-channel! filepath
                                    :character state))
             (state (pprinted-lines-to-channel lines channel state))
             (state (close-output-channel channel state)))
          (acl2::value nil)))))