		Search-engine friendly clone of the ACL2 documentation.

Svtv-doc

Stv-entry-to-xml

Encode a single value from an STV line.

Signature
(stv-entry-to-xml entry expansion acc) → acc
Arguments: entry — The value that the user gave, originally.; expansion — Its expanded out value, a sexpr list.
Guard (or (not expansion) (svtv-entry-p expansion)).
Returns: acc — Type (character-listp acc), given (character-listp acc).

Definitions and Theorems

Function: stv-entry-to-xml

(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: character-listp-of-stv-entry-to-xml

(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)