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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
