		Search-engine friendly clone of the ACL2 documentation.

Vl-basic-fmt

Vl-fmt-tilde-x

Signature
(vl-fmt-tilde-x x &key (ps 'ps)) → ps

Definitions and Theorems

Function: vl-fmt-tilde-x-fn

(defun vl-fmt-tilde-x-fn (x ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-fmt-tilde-x))
  (declare (ignorable __function__))
  (b*
   ((rchars (vl-ps->rchars))
    (col (vl-ps->col))
    (pkg (vl-ps->package))
    (base (vl-ps->base))
    (htmlp (vl-ps->htmlp))
    (tabsize (vl-ps->tabsize))
    (rmargin (vl-ps->autowrap-col))
    (xevisc (str::eviscerate x (vl-ps->eviscconfig)))
    (config (str::make-printconfig
                 :flat-right-margin (max 40 (floor rmargin 2))
                 :hard-right-margin (max 77 rmargin)
                 :print-base base
                 :print-radix nil
                 :home-package pkg
                 :print-lowercase nil))
    (x-rchars (str::revappend-pretty xevisc nil
                                     :config config
                                     :col col
                                     :eviscp t))
    ((unless htmlp)
     (vl-ps-seq
         (vl-ps-update-rchars (cons (str::rchars-to-string x-rchars)
                                    rchars))
         (vl-ps-update-col (vl-fmt-tilde-x-column x-rchars col))))
    ((mv col rchars)
     (str::html-encode-chars-aux (reverse x-rchars)
                                 col tabsize rchars)))
   (vl-ps-seq (vl-ps-update-col col)
              (vl-ps-update-rchars rchars)))))