		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-file-to-filesystem

Pretty-print a file to the file system.

Signature
(pprint-file-to-filesystem file include options filepath state) → (mv erp val state)
Arguments: file — Guard (filep file).; include — Guard (maybe-stringp include).; options — Guard (pprint-options-p options).; filepath — Guard (stringp filepath).

We pretty-print the lines and then we write them to the file path.

Definitions and Theorems

Function: pprint-file-to-filesystem

(defun pprint-file-to-filesystem
       (file include options filepath state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (filep file)
                              (maybe-stringp include)
                              (pprint-options-p options)
                              (stringp filepath))))
  (let ((__function__ 'pprint-file-to-filesystem))
    (declare (ignorable __function__))
    (pprinted-lines-to-file (pprint-file file include options)
                            filepath state)))