String.substring() question

[Tom Tromey <tromey at redhat dot com>]

Right now String.substring() always creates a reference to the old
string's data.  I wonder if that is always what we want.  I think
perhaps if the old String is very large and the new substring is very
small, then we might consider making a copy.  Or maybe for very large
Strings we could consider playing some game involving weak references?
Or maybe this is a nonissue -- maybe people don't make huge Strings
often enough for it to be worthwhile.

I'm not aware of any data that would help us make these sorts of
decisions.  Bummer.

Tom