makarius at sketis.net
Thu May 30 23:27:04 CEST 2013
There is a funny comment here:
(* Isabelle does not use vectors? *)
Isn't live nice without vectors, arrays, a host of "int" types that are
not int at all?
The one exception is src/Pure/Syntax/parser.ML, where arrays are used
internally due to some historic "optimization". It probably wastes a lot
of space, since every grammar update needs a fresh copy of the whole
Working routinely on the JVM now (due to Scala), I've found so many
inefficiencies in the libraries due to the historic predominance of these
mutable bulk data structures (aka arrays). This is particularly bad when
working with plain text, aka strings.
More information about the isabelle-dev