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



On Wed, 19 Nov 2014, Michael Norrish wrote:

On 19/11/14 03:28, Makarius wrote:

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.

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>".

That is an application of generating sources, which could be easily changed to emit "\027\027<forall>" instead.


BTW, "malformed symbol" above only refers to \< not a proper \<forall>, but "\\<forall>" is also rejected due to the way how sources are passed through the system: text is always treated at Isabelle symbol boundaries.

This is the reason why the Prover IDE works with symbols at all. The UTF-8 that is occasionally seen in Coq sources does not work in that respect.


In any case, I would like to see real applications and real problems. Then one can find ways to make it work. In contrast, the general problem of adding Unicode support everywhere and uniformly cannot be solved.


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.

Such things can be made to suck less in a case-by-case basis. I am doing it myself whenever it is feasible, but the general problem remains. E.g. when you drag-and-drop files on some application, it depends on many side-conditions of the operating system desktop what really happens.


	Makarius

----------------------------------------------------------------------------
                  http://stop-ttip.org  912,049 people so far
----------------------------------------------------------------------------




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