		Search-engine friendly clone of the ACL2 documentation.

Svtv-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 (or (not expansion) (svtv-line-p 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)
                             (or (not expansion)
                                 (svtv-line-p 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)
                                (and expansion
                                     (svtv-line->entries 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)