[isabelle-dev] Lexical structure of ML strings

[Florian Haftmann]

I have some doubt whether the parsing of strings by Isabelle/ML conforms
to plain ML.

See the following examples.

ML_val ‹
val s = "a\nb";
writeln s;
›

OK, seems quite plausible.

ML_val ‹
val s = "a\\b";
writeln s;
›

OK, seems quite plausible.

ML_val ‹
val s = "a\\<^isub>1";
writeln s;
›

This gives a lexical error, though I guess it should interpret as plain
"a\<^isub>1".  (Alas I have no suitable literature at hand which would
give an exact specification of a string's lexical structure in ML).

So, is this the intended behaviour?  I have stumbled over that issue
while trying to generate code involvings strings of that kind.

Any suggestions welcome.

Thanks a lot,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20150126/b082d63a/attachment.asc>