		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-fileset

Pretty-print a file set to the file system.

Signature
(pprint-fileset fileset file-name options state) → (mv erp val state)
Arguments: fileset — Guard (filesetp fileset).; file-name — Guard (stringp file-name).; options — Guard (pprint-options-p options).

We pretty-print each file in the fileset, at the associated path. For now we cause an error if there is a header (which should not be there, but we will add support soon), and we just generate the source file, by appending the .c extension to the path without extension.

Definitions and Theorems

Function: pprint-fileset

(defun pprint-fileset (fileset file-name options state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (filesetp fileset)
                             (stringp file-name)
                             (pprint-options-p options))))
 (let ((__function__ 'pprint-fileset))
  (declare (ignorable __function__))
  (b* ((path-wo-ext (fileset->path-wo-ext fileset)))
   (if
    (fileset->dot-h fileset)
    (b* (((er &)
          (pprint-file-to-filesystem
               (fileset->dot-h fileset)
               nil options (str::cat path-wo-ext ".h")
               state)))
      (pprint-file-to-filesystem (fileset->dot-c fileset)
                                 (str::cat file-name ".h")
                                 options (str::cat path-wo-ext ".c")
                                 state))
    (pprint-file-to-filesystem
         (fileset->dot-c fileset)
         nil options (str::cat path-wo-ext ".c")
         state)))))