dataBuffer [dataBufferPos++] = c;
    private void dataBufferAppend (char c)    {	// Expand buffer if necessary.	if (dataBufferPos >= dataBuffer.length)	    dataBuffer =		(char[]) extendArray (dataBuffer,			dataBuffer.length, dataBufferPos);	dataBuffer [dataBufferPos++] = c;    }