On 19/09/2016 21:54, Makarius wrote:
On 16/09/16 14:24, David Matthews wrote:

The representation of strings has been simplified.  Previously, single
character strings were represented by the character itself as a tagged
value.  This was largely a relic of SML 90 which didn't have a separate
char type.  That has been removed and all strings are now represented as
a vector of bytes.  This speeds up string operations since the code no
longer has to consider the special case.

It should be actually easy for Isabelle/ML to cope with the new
representation of Poly/ML, using a table of pre-allocated singleton
strings. I have done something similar for the Isabelle/Scala version of
Symbol.explode, since the JVM is based on legacy UTF-16 widestring

I can do the same for the Isabelle/ML library, but there might be a
general benefit if basis/String.sml would do it uniformly in
charAsstring and thus in String.str etc.

Instead of creating a new singleton string each time, it would refer to
a vector of 256 pre-allocated values.

That seems a very good idea.  I've implemented it.


polyml mailing list

Reply via email to