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