		Search-engine friendly clone of the ACL2 documentation.

Stv-doc

Stv-line-to-xml

Encode one full line from the STV into XML for XDOC.

Signature
(stv-line-to-xml line expansion acc) → acc
Arguments: line — Original line, with name, given by the user.
Guard (true-listp line).; expansion — Fully expanded line, with name, after STV processing.
Guard (true-listp expansion).
Returns: acc — Type (character-listp acc), given (character-listp acc).

Definitions and Theorems

Function: stv-line-to-xml

(defun stv-line-to-xml (line expansion acc)
  (declare (xargs :guard (and (true-listp line)
                              (true-listp expansion))))
  (let ((__function__ 'stv-line-to-xml))
    (declare (ignorable __function__))
    (b* ((acc (str::revappend-chars "<stv_line>" acc))
         (acc (str::revappend-chars "<stv_name>" acc))
         (acc (stv-name-to-xml (car line) acc))
         (acc (str::revappend-chars "</stv_name>" acc))
         (acc (stv-entries-to-xml (cdr line)
                                  (cdr expansion)
                                  acc))
         (acc (str::revappend-chars "</stv_line>" acc))
         (acc (cons #\Newline acc)))
      acc)))

Theorem: character-listp-of-stv-line-to-xml

(defthm character-listp-of-stv-line-to-xml
  (implies (character-listp acc)
           (b* ((acc (stv-line-to-xml line expansion acc)))
             (character-listp acc)))
  :rule-classes :rewrite)