|
|
|---|
|
|
|
|---|
Routines to encode HTML entities such as
In principle, this conversion may not be entirely legitimate in the sense of any particular HTML specification, since ACL2 strings might contain non-printable characters or other similarly unlikely garbage. But it seems like what we implement is pretty reasonable.
We convert newline characters into the sequence