[isabelle-dev] Lexical structure of ML strings

[Christian Sternagel]

I think the following thread is related to your question:

http://comments.gmane.org/gmane.science.mathematics.logic.isabelle.user/10007

On 01/26/2015 09:30 AM, Florian Haftmann wrote:
> 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
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>