[isabelle-dev] Spec_Check

[Makarius]

There is a funny comment here:
http://isabelle.in.tum.de/repos/isabelle/file/cdba0c3cb4c2/src/HOL/Spec_Check/base_generator.ML#l94

   (* 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 
thing.

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.


 	Makarius