private final void push(int ch) {
		if (ch != 0) {
			if (mTextPos == mTextBuffer.length) {
				char[] bigger = new char[mTextPos * 4 / 3 + 4];

				System.arraycopy(mTextBuffer, 0, bigger, 0, mTextPos);
				mTextBuffer = bigger;
			}
			mTextBuffer[mTextPos++] = (char) ch;
		}
	}