Encode a single value from an STV line.
(stv-entry-to-xml entry expansion acc) → acc
Function:
(defun stv-entry-to-xml (entry expansion acc) (declare (xargs :guard (or (not expansion) (svtv-entry-p expansion)))) (let ((__function__ 'stv-entry-to-xml)) (declare (ignorable __function__)) (cond ((4vec-p expansion) (revappend (4vec-to-xml-chars expansion) acc)) ((svtv-dontcare-p entry) acc) ((symbolp entry) (b* ((acc (str::revappend-chars "<b>" acc)) ((mv ?col acc) (str::html-encode-string-aux (symbol-name entry) 0 (length (symbol-name entry)) 0 8 acc)) (acc (str::revappend-chars "</b>" acc))) acc)) ((svtv-condoverride-p entry) (b* (((svtv-condoverride entry)) ((unless (and (symbolp entry.value) (symbolp entry.test))) acc) (acc (str::revappend-chars "<b>" acc)) ((mv ?col acc) (str::html-encode-string-aux (symbol-name entry.value) 0 (length (symbol-name entry.value)) 0 8 acc)) (acc (str::revappend-chars "</b>" acc))) acc)) (t (raise "Bad entry in stv line: ~x0." entry)))))
Theorem:
(defthm character-listp-of-stv-entry-to-xml (implies (character-listp acc) (b* ((acc (stv-entry-to-xml entry expansion acc))) (character-listp acc))) :rule-classes :rewrite)