/*
     * Shrinks the storage from a hashtable to an array.
     */
    private void shrink() {
        Hashtable tmp = (Hashtable)table;
        Object[] array = new Object[tmp.size()*2];
        Enumeration keys = tmp.keys();
        int j = 0;
	
        while (keys.hasMoreElements()) {	    
            Object o = keys.nextElement();
            array[j] = o;
            array[j+1] = tmp.get(o);
            j+=2;
        }
        table = array;	
    }
}