[isabelle-dev] Lexical structure of ML strings

[Florian Haftmann]

> I think the following thread is related to your question:
> 
> http://comments.gmane.org/gmane.science.mathematics.logic.isabelle.user/10007

I see.  I think it is best if I find a possibility to print strings in a
way that is both digestible for Isabelle/ML and (S)ML.

	Florian

> 
> 
> 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
>>
>>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-- 

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://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150126/c8e8cc75/attachment.sig>