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 representation.
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.
Regards, David