• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
      • Std/strings
        • Pretty-printing
        • Printtree
        • Base64
        • Charset-p
        • Strtok!
        • Cases
        • Concatenation
        • Html-encoding
          • Html-encode-string-aux
          • Html-encode-chars-aux
          • Html-encode-push
          • Html-encode-string-basic-aux
          • Html-encode-string
          • Html-encode-char-basic
          • Html-encode-chars-basic-aux
          • Html-encode-string-basic
        • Character-kinds
        • Substrings
        • Strtok
        • Equivalences
        • Url-encoding
        • Lines
        • Ordering
        • Numbers
        • Pad-trim
        • Coercion
        • Std/strings-extensions
        • Std/strings/digit-to-char
        • Substitution
        • Symbols
      • Std/io
      • Std/osets
      • Std/system
      • Std/basic
      • Std/typed-lists
      • Std/bitsets
      • Std/testing
      • Std/typed-alists
      • Std/stobjs
      • Std-extensions
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Testing-utilities
    • Math
  • Std/strings

Html-encoding

Routines to encode HTML entities, e.g., < becomes &lt;.

In principle, our conversion routines may not be entirely legitimate in the sense of some precise HTML specification, because we do not account for non-printable characters or other similarly unlikely garbage in the input. But it seems like what we implement is pretty reasonable, and handles most ordinary characters.

Note that we convert #\Newline characters into the sequence <br/>#\Newline. This may not be the desired behavior in certain applications, but seems basically reasonable for converting plain text into HTML.

Subtopics

Html-encode-string-aux
Core of converting strings into HTML, output to an accumulator.
Html-encode-chars-aux
Convert a character list into HTML. Outputs to an accumulator. Tracks the column number to handle tab characters.
Html-encode-push
HTML encode a single character, with column/tabsize support.
Html-encode-string-basic-aux
Convert a string into HTML (simple version, no tab support).
Html-encode-string
(html-encode-string x tabsize) converts the string x into HTML, and returns the result as a new string. Tracks the column number to handle tab characters.
Html-encode-char-basic
HTML encode a single character (simple version, no tab support).
Html-encode-chars-basic-aux
Convert a character list into HTML (simple version, no column/tabsize support).
Html-encode-string-basic
Convert a string into HTML (simple version, no tab support).