History log of /seL4-l4v-master/HOL4/src/parse/MLstring.sml
Revision Date Author Comments
# f6f5ded6 27-Jul-2006 Michael Norrish <Michael.Norrish@nicta.com.au>

String literals are now lexed in accordance with SML rules. That means
things like
``"\t\000\u004f"``
are possible. There are three things to watch out for. The syntax for
control characters has to double the ^ symbol. Thus
``"\^^C"``
for CHR 3. This is just a generalisation of the rule that says ^ has to be
doubled everywhere. I.e., you also have to write ``"^^"`` to get a string
containing a single caret. Similarly, you have to ^-escape the ` symbol
wherever it may occur.
Finally, the SML syntax for breaking long strings over multiple lines
won't work until I mess with the quotation filter again. In other words,
you can't yet write
``"hello \
\there"``
and have it work (yet).