		Search-engine friendly clone of the ACL2 documentation.

Printing-locally

Vl-ps-save-config

Save the current configuration of ps into a vl-psconfig-p object.

Signature
(vl-ps-save-config &key (ps 'ps)) → config
Returns: config — Type (vl-psconfig-p config).

Note that this does not save the currently-printed text and column number; only the configuration settings are saved.

Definitions and Theorems

Function: vl-ps-save-config-fn

(defun vl-ps-save-config-fn (ps)
       (declare (xargs :stobjs (ps)))
       (declare (xargs :guard t))
       (let ((__function__ 'vl-ps-save-config))
            (declare (ignorable __function__))
            (make-vl-psconfig :autowrap-col (vl-ps->autowrap-col)
                              :autowrap-ind (vl-ps->autowrap-ind)
                              :htmlp (if (vl-ps->htmlp) t nil)
                              :tabsize (vl-ps->tabsize)
                              :package (vl-ps->package)
                              :base (vl-ps->base)
                              :eviscconfig (vl-ps->eviscconfig))))

Theorem: vl-psconfig-p-of-vl-ps-save-config

(defthm vl-psconfig-p-of-vl-ps-save-config
        (b* ((config (vl-ps-save-config-fn ps)))
            (vl-psconfig-p config))
        :rule-classes :rewrite)