Re: [isabelle] Potential Spam: Isabelle/PIDE as IDE for Standard ML

On 19/11/14 03:28, Makarius wrote:
> On Tue, 18 Nov 2014, Michael Norrish wrote:

>> The lexeme "\<forall>" is not a valid string literal in SML (Poly, mlton and
>> Moscow ML, certainly agree with me), but it's fine in a file being interpreted
>> with SML_file.

> That is not a "lexeme", but an "Isabelle symbol".  This concept is below the
> lexical syntax, like \uXXXX in Java.  It is documented in the "implementation"
> and "isar-ref" manual.

I appreciate that all of these notions make sense in the context of Isabelle.
All of my criticisms are of the IDE in the context of developing SML rather than

>> The SML_file mode also rejects "\\<" as a string literal, which is incorrect.

> Formally that is a "malformed symbol".  One could try harder to accept that. 
> The question is if this is of practical relevance.  Are there concrete SML
> programs where this happens?

Indeed, any SML program attempting to emit Isabelle symbols in a way that is
valid SML may want to contain string literals like "\\<forall>".

> We don't have millions of SML projects around.  So it might be simpler to change
> these, e.g. by using "\\" ^ "<".

Of course there are workarounds.  I just hesitate to recommend a tool for
general SML usage that doesn't quite implement SML.

> Unicode file-names are a sure way to ask for trouble.  In conjunction with the
> "portable" JVM things are particularly fragile.  I have seen routine problems
> with Far Eastern file names on Windows and sometimes Linux. There are also
> problems with continental European diacritics on Windows.

I adjusted the seL4 C parser precisely to cope with Chinese in filenames (a
user-reported problem).  So, yes, there was a problem with a Unicode filename,
but luckily, I could create a system that worked.  The files were part of a C
project that clearly did work in that context.  If the C infrastructure could
cope with Unicode filenames, I felt I should try too.


Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.