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

Some minor criticisms: the Isabelle/ML handling of string constants is
contaminating SML in this mode.

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.

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

Similarly, the string literal "∀" (UTF-8 encoding) is interpreted as if it were
"\<forall>".  It's perhaps arguable what SML really requires of "∀":  mlton and
Poly/ML both see it as an error; Moscow ML accepts it as a string of size 3.  If
mlton and Poly/ML were to accept it, I expect they would follow Moscow ML and

    "∀" = "\226\136\128"

to true.  The SML_file facility does not.

Worse, if I load a file with a genuine occurrence of the UTF-8 encoded "∀", then
the IDE will silently write it out to disk as "\<forall>" when the file is
saved.  This even happens if the ∀ occurs bare in a comment.  I find this

More importantly, only some special characters get this treatment.  If I write

    String.explode "大学";

the IDE (at least on my machine) just displays black boxes in the edit window,
but does decompose the sequence into the UTF-8 encoding as chars:

    val it = [#"\229", #"\164", #"\167", #"\229", #"\173", #"\166"]: char list

So, not only is the SML mode perhaps deviating from the standard by accepting
string literals like "∀" and "大学", but it's doing so in a confusing way: some
string literals are silently turned into \<....> forms, and others are not.

Note that this is also a minor annoyance in Isabelle proper.  Users can't access
files called ∀.c by passing that name as written to an Isabelle/ML routine.
Instead they have to write  \226\136\128.c


On 18/11/14 07:46, Makarius wrote:
> Dear Isabelle users,
> the current Isabelle2014 has this built-in PIDE support for official Standard ML
> (SML'97) that was already mentioned a few times before; it is briefly explained
> in the NEWS of the distribution.
> I would like to publicize this as much as possible.  It could help the general
> cause of Standard ML (the best unknown programming language in the world) and in
> particular Poly/ML (the best unknown implementation of SML).
> Here is the corresponding entry on my new website/blog:
> This is a permanent link that can be used elsewhere, despite the slightly odd
> name, which is normal in WordPress, I think.  Of course, enthusiastic users are
> encouraged to publish their own texts about the SML IDE.
> My blog mentions a sister entry on Stackoverflow:
> I don't want to bribe anybody, but maybe we could collect a few more votes for
> that article so that it is higher ranked.  This is relevant, because Google
> presently places it first for a query like "SML IDE".
>     Makarius
> ----------------------------------------------------------------------------
>            906,830 people so far
> ----------------------------------------------------------------------------

Attachment: signature.asc
Description: OpenPGP digital signature

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