		Search-engine friendly clone of the ACL2 documentation.

Reader

Fancy-string-reader

A friendly syntax for strings literals that have backslashes and quotes.

Examples:

ACL2 !> #{"""Hello, World!"""}
"Hello, World!"

ACL2 !> #{"""<img src="hello.png"/>"""}
"<img src=\"hello.png\"/>"

ACL2 !> #{"""C:\ACL2\axioms.lisp"""}
"C:\\ACL2\\axioms.lisp"

String literals in ACL2 and Common Lisp source code files are usually written as text strings within quote marks. For instance, the 5-character string whose contents are Hello is normally written as "Hello".

Usually this syntax is fine, but things can get tricky when you want to write a string whose contents include " marks. For example, if you wanted to write down a string whose contents were:

<img src="hello.png"/>

then you would need to escape the quote marks within it using backslash characters, e.g., as follows:

"<img src=\"hello.png\"/>"

But using \ as a special character means we also need a special way to write backslashes. For instance, if we want to write a string literal whose contents are:

C:\ACL2\axioms.lisp

Then we would need to write something a string literal such as:

"C:\\ACL2\\axioms.lisp"

In certain cases, such as when writing long documentation strings, the extra escaping can be tedious and error-prone.

To simplify this, ACL2 provides an alternate #{"""..."""} syntax for string literals. This syntax has no special characters, so nothing needs to be escaped. The end of the string is recognized by the unusual character sequence """}.

In the rare case that you need to have the sequence """} in your string, you can instead use """\}. If you need to have the sequence """\}, you can use """\\}. In general, when a substring contains three doublequotes followed by 1 or more backslashes and a right curlybrace, it just removes one of the backslashes.