		Search-engine friendly clone of the ACL2 documentation.

Html-encoding

Vl-html-encode-string-aux

Print an HTML encoded string, efficiently, without exploding it.

Signature
(vl-html-encode-string-aux x n xl col tabsize acc) → (mv new-col new-acc)
Arguments: x — Guard (stringp x).; n — Guard (natp n).; xl — Guard (eql xl (length x)).; col — Guard (natp col).; tabsize — Guard (posp tabsize).

We just leave this enabled since its logical definition is so simple.

Definitions and Theorems

Function: vl-html-encode-string-aux

(defun vl-html-encode-string-aux (x n xl col tabsize acc)
  (declare (xargs :guard (and (stringp x)
                              (natp n)
                              (natp col)
                              (posp tabsize)
                              (eql xl (length x)))))
  (declare (type string x)
           (type integer n xl col tabsize))
  (declare (xargs :split-types t :guard (<= n xl)))
  (let ((__function__ 'vl-html-encode-string-aux))
    (declare (ignorable __function__))
    (mbe :logic
         (vl-html-encode-chars-aux (nthcdr n (explode x))
                                   col tabsize acc)
         :exec
         (b* (((when (mbe :logic (zp (- (nfix xl) (nfix n)))
                          :exec (eql n xl)))
               (mv (lnfix col) acc))
              (char1 (char x n))
              (acc (vl-html-encode-push char1 col tabsize acc))
              (col (vl-html-encode-next-col char1 col tabsize)))
           (vl-html-encode-string-aux x (+ 1 (lnfix n))
                                      xl col tabsize acc)))))