// Precondition: checkInitialization has been called.
private void enlargeHashTable()
{
   TableEntry<K, V>[] oldTable = hashTable;
   int oldSize = hashTable.length;
   int newSize = getNextPrime(oldSize + oldSize);
   checkSize(newSize);

   // The cast is safe because the new array contains null entries
   @SuppressWarnings("unchecked")
   TableEntry<K, V>[] temp = (TableEntry<K, V>[])new TableEntry[newSize]; // Increase size of array
   hashTable = temp;
   numberOfEntries = 0; // Reset number of dictionary entries, since
                        // it will be incremented by add during rehash

   // Rehash dictionary entries from old array to the new and bigger array;
   // skip both null locations and removed entries
   for (int index = 0; index < oldSize; index++)
   {
      if ( (oldTable[index] != null) && oldTable[index].isIn() )
         add(oldTable[index].getKey(), oldTable[index].getValue());
   } // end for
} // end enlargeHashTable
// Version 4.0