		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-maybe-update-filemap

Signature
(vl-maybe-update-filemap realfile contents ppst) → ppst
Arguments: realfile — Guard (stringp realfile).; contents — Guard (vl-echarlist-p contents).

Definitions and Theorems

Function: vl-maybe-update-filemap

(defun vl-maybe-update-filemap (realfile contents ppst)
  (declare (xargs :stobjs (ppst)))
  (declare (xargs :guard (and (stringp realfile)
                              (vl-echarlist-p contents))))
  (let ((__function__ 'vl-maybe-update-filemap))
    (declare (ignorable __function__))
    (b* (((vl-loadconfig config)
          (vl-ppst->config))
         ((unless config.filemapp) ppst)
         (filemap (vl-ppst->filemap))
         ((when (assoc-equal realfile filemap))
          ppst)
         (filemap (cons (cons realfile
                              (vl-echarlist->string contents))
                        filemap)))
      (vl-ppst-update-filemap filemap))))