		Search-engine friendly clone of the ACL2 documentation.

Json-encoders

Vl-jp-warning

Special, custom JSON encoder for warnings.

Signature
(vl-jp-warning x &key (ps 'ps)) → ps
Arguments: x — Guard (vl-warning-p x).

We probably don't want to use the ordinary aggregate-encoding stuff to print vl-warning-p objects, since the types in the :args field are dynamic and, besides, who wants to reimplement vl-cw in other languages. Instead, it's probably more convenient to just go ahead and convert the warning into a printed message here. We'll include both HTML and plain TEXT versions of the message.

Definitions and Theorems

Function: vl-jp-warning-fn

(defun vl-jp-warning-fn (x ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (vl-warning-p x)))
  (let ((__function__ 'vl-jp-warning))
    (declare (ignorable __function__))
    (b* (((vl-warning x) x)
         (text (with-local-ps (vl-cw-obj x.msg x.args)))
         (html (with-local-ps (vl-ps-update-htmlp t)
                              (vl-ps-update-autowrap-col 100000)
                              (vl-cw-obj x.msg x.args))))
      (jp-object :tag (vl-print "\"warning\"")
                 :fatalp (jp-bool x.fatalp)
                 :type (jp-str (symbol-name x.type))
                 :fn (jp-str (symbol-name x.fn))
                 :text (jp-str text)
                 :html (jp-str html)))))