		Search-engine friendly clone of the ACL2 documentation.

Json-encoders

Jp-str

Print the JSON encoding of a string, handling all escaping correctly and including the surrounding quotes.

Signature
(jp-str x &key (ps 'ps)) → ps

We go to some effort to make this fast.

Definitions and Theorems

Function: jp-str-fn

(defun jp-str-fn (x ps)
 (declare (xargs :stobjs (ps)))
 (declare (type string x))
 (let ((__function__ 'jp-str))
  (declare (ignorable __function__))
  (b*
   ((rchars (vl-ps->rchars))
    (col (vl-ps->col))
    (xl (length x))
    (rchars
      (cons #\"
            (bridge::json-encode-str-aux x 0 xl (cons #\" rchars))))
    (col (+ 2
            (jp-col-after-printing-string-aux col x 0 xl))))
   (vl-ps-seq (vl-ps-update-rchars rchars)
              (vl-ps-update-col col)))))

Subtopics

Jp-col-after-printing-string-aux: Fast way to figure out the new column after printing a JSON string with proper encoding.