org.eclipse.ui.console/src/org/eclipse/ui/internal/console/ConsoleDocumentAdapter.java

/*******************************************************************************
 * Copyright (c) 2000, 2019 IBM Corporation and others.
 *
 * This program and the accompanying materials
 * are made available under the terms of the Eclipse Public License 2.0
 * which accompanies this distribution, and is available at
 * https://www.eclipse.org/legal/epl-2.0/
 *
 * SPDX-License-Identifier: EPL-2.0
 *
 * Contributors:
 *     IBM Corporation - initial API and implementation
 *     Paul Pazderski  - Bug 544970: reimplementation with correct text change event calculation
 *******************************************************************************/
package org.eclipse.ui.internal.console;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.List;

import org.eclipse.core.runtime.Assert;
import org.eclipse.jface.text.BadLocationException;
import org.eclipse.jface.text.DocumentEvent;
import org.eclipse.jface.text.IDocument;
import org.eclipse.jface.text.IDocumentAdapter;
import org.eclipse.jface.text.IDocumentListener;
import org.eclipse.jface.text.IRegion;
import org.eclipse.jface.text.MultiStringMatcher;
import org.eclipse.jface.text.MultiStringMatcher.Match;
import org.eclipse.jface.text.Region;
import org.eclipse.swt.custom.TextChangeListener;
import org.eclipse.swt.custom.TextChangedEvent;
import org.eclipse.swt.custom.TextChangingEvent;
import org.eclipse.ui.console.ConsolePlugin;

/**
 * Adapts a Console's document to the viewer StyledText widget. Allows proper
 * line wrapping of fixed width consoles without having to add line delimiters
 * to the StyledText.
 *
 * By using this adapter, the offset of any character is the same in both the
 * widget and the document.
 *
 * <p>
 * Note: tab character (\t) is not handled special and counts as one character.
 * So wrapped content may look less fixed width if it contains tab characters.
 * </p>
 *
 * @since 3.1
 */
public class ConsoleDocumentAdapter implements IDocumentAdapter, IDocumentListener {
	/*
	 * Because of the fixed width feature this adapter knows two types of lines.
	 * Document lines are lines as known to the adapted document and are terminated
	 * by a line delimiter (except for the last line). Widget lines are lines as
	 * seen in the text viewer. If a document line is wrapped due to fixed width it
	 * starts a new widget line. Widget lines generated by line wrapping do not have
	 * additional line delimiters. If fixed width is disabled widget line and
	 * document line are the same.
	 */

	/**
	 * If <code>true</code> the adapter will check if the predicted document change
	 * calculated for the TextChangingEvent matches the document after the applied
	 * change. Useful for developing/debugging.
	 */
	private static final boolean ASSERT = false;

	/**
	 * If {@link #widgetLineOffsets} need to grow add some extra space to prevent
	 * frequent array copies.
	 */
	private static final int GROW = 500;

	/** Registered {@link TextChangeListener}s. */
	private final List<TextChangeListener> textChangeListeners = new ArrayList<>();

	/** Fixed console width. If &lt;= 0 fixed console mode is disabled. */
	private int fixedConsoleWidth;

	/** Adapted document. */
	private IDocument document;
	/**
	 * The matcher to find the legal line delimiters of the connected document in
	 * some text. <code>null</code> if no document connected.
	 * <p>
	 * This usually matches <code>{ "\r", "\n", "\r\n" }</code>.
	 * </p>
	 */
	private MultiStringMatcher docLegalLineDelimiterMatcher;

	/**
	 * Number of widget lines in document. If fixed width is disabled it is always
	 * equal to {@link IDocument#getNumberOfLines()}. If fixed width mode is enabled
	 * there may be more widget lines then doc lines but never less.
	 */
	private int widgetLines;

	/**
	 * Start offsets of widget lines.
	 * <p>
	 * <b>Note:</b> offsets are only valid and updated if fixed width is enabled.
	 * </p>
	 * <p>
	 * Example content: if the document contains the following content (with
	 * <code>\r\n</code> as line delimiter)
	 *
	 * <pre>
	 *     0123456789ABCD\r\n
	 *     ---\r\n
	 *     0123456789
	 * </pre>
	 *
	 * a fixed width of <code>10</code> the widget will show it as
	 *
	 * <pre>
	 *     0123456789
	 *     ABCD\r\n
	 *     ---\r\n
	 *     0123456789
	 * </pre>
	 *
	 * the content of the {@link #widgetLineOffsets} array is:
	 * <code>{ 0, 10, 16, 21 }</code> which represent the start offsets from each of
	 * the four widget lines.
	 * </p>
	 * <p>
	 * Initialized with one element to save memory in non fixed width mode but at
	 * the same time prevent NPE.
	 * </p>
	 *
	 * @see #isFixedWidth()
	 * @see #ensureOffsetsCapacity(int)
	 */
	private int[] widgetLineOffsets = new int[1];

	/**
	 * The fact that wrapped lines are new lines without a newline delimiter leads
	 * to some hard to handle edge cases since all involved interfaces (implicit)
	 * assume a newline has its unique offset.
	 * <p>
	 * Consider a fixed with of 10 and a console filled with (automatically wrapped)
	 * content of:
	 * </p>
	 *
	 * <pre>
	 * 0123456789
	 * 0
	 * </pre>
	 *
	 * <p>
	 * If we remove the last character ('0') we must set replaceLineCount to 1 since
	 * there is one line less due to the unwrapped line. The replaceLineCount is
	 * necessary so that StyledTextRenderer updates the lines which possible follow
	 * below and have changed due to moved content.
	 * </p>
	 * <p>
	 * But StyledTextRenderer presumes that the line index where the event occurs is
	 * the same before and after the text change. This is not the case for our auto
	 * wrapped lines since getLineAtOffset(10) is 1 before text change and 0 after
	 * </p>
	 * <p>
	 * To solve this unlucky situation we will lie to StyledText(Renderer) for the
	 * short time between text changing event and actual text change. If we know the
	 * same (start) offset will yield a different line index before and after change
	 * we will return for this offset the line index it will have after the change
	 * already before the change is applied. In this example if StyledText ask for
	 * getLineAtOffset(10) we return 0 already before the text is actual changed.
	 * </p>
	 * <p>
	 * This field store the offset for which we should preempt the new line index.
	 * It must be an offset at fixed width border (or negative for none) because
	 * only those have the potential for two different line indexes at same offset.
	 * </p>
	 */
	private int preemptLineWrapChange = -1;

	/**
	 * New {@link ConsoleDocumentAdapter} with no {@link IDocument} connected yet.
	 *
	 * @param width fixed console width to enforce text wrap or &lt;= 0 to disable
	 *              fixed console width
	 */
	public ConsoleDocumentAdapter(int width) {
		setWidth(width);
	}

	@Override
	public void setDocument(IDocument doc) {
		if (document != null) {
			document.removeDocumentListener(this);
		}

		document = doc;
		docLegalLineDelimiterMatcher = null;
		updateWidgetOffsets(0);

		if (doc != null) {
			doc.addDocumentListener(this);
			docLegalLineDelimiterMatcher = MultiStringMatcher.create(doc.getLegalLineDelimiters());
		}
	}

	@Override
	public synchronized void addTextChangeListener(TextChangeListener listener) {
		Assert.isLegal(listener != null, "listener null"); //$NON-NLS-1$
		if (!textChangeListeners.contains(listener)) {
			textChangeListeners.add(listener);
		}
	}

	@Override
	public synchronized void removeTextChangeListener(TextChangeListener listener) {
		Assert.isLegal(listener != null, "listener null"); //$NON-NLS-1$
		textChangeListeners.remove(listener);
	}

	@Override
	public int getCharCount() {
		return document.getLength();
	}

	@Override
	public String getLine(int lineIndex) {
		try {
			final IRegion lineRegion = getLineInformation(lineIndex);
			return document.get(lineRegion.getOffset(), lineRegion.getLength());
		} catch (BadLocationException e) {
			log(e);
			return ""; //$NON-NLS-1$
		}
	}

	/**
	 * Return information about a widget line.
	 * <p>
	 * Note: in contrast to some implementations of
	 * {@link org.eclipse.jface.text.ILineTracker#getLineInformation(int)} this
	 * implementation throws an exception if line after last line is queried.
	 * </p>
	 *
	 * @param widgetLineIndex the widget line number (first line has number 0)
	 * @return the lines start offset and length excluding line delimiter
	 * @throws BadLocationException if widget line does not exist
	 * @see IDocument#getLineInformation(int)
	 */
	private IRegion getLineInformation(int widgetLineIndex) throws BadLocationException {
		if (!isFixedWidth()) {
			return document.getLineInformation(widgetLineIndex);
		}

		final int widgetLineOffset = getLineOffset(widgetLineIndex);
		final IRegion docLine = document.getLineInformationOfOffset(widgetLineOffset);
		// widget line length is calculated as: length of containing document line
		int widgetLineLength = docLine.getLength();
		// minus preceding wrapped lines
		widgetLineLength -= (widgetLineOffset - docLine.getOffset());
		// now widgetLinelength is length from widget line start offset until real
		// document line end. If widgetLinelength is still greater than
		// fixedConsoleWidth there are more wrapped content after this widget line
		// therefore this widget line length must equal fixedConsoleWidth otherwise it
		// is the length of requested widget line.
		widgetLineLength = Math.min(widgetLineLength, fixedConsoleWidth);
		return new Region(widgetLineOffset, widgetLineLength);
	}

	@Override
	public int getLineAtOffset(int offset) {
		try {
			return getLineOfOffset(offset);
		} catch (BadLocationException e) {
			log(e);
			// Note: this strange return value is inherited from the previous implementation
			// of this method which did no boundary checks on the offset and either returned
			// the first or last line index for bad locations.
			return offset < 0 ? 0 : widgetLines - 1;
		}
	}

	/**
	 * Return the widget line index at the given character offset.
	 * <p>
	 * Like {@link #getLineAtOffset(int)} but throws exception in case of invalid
	 * offset.
	 * </p>
	 *
	 * @param offset offset in document
	 * @return the number of the widget line at offset (0 for first line)
	 * @throws BadLocationException if the offset is invalid in adapted document
	 * @see #getLineAtOffset(int)
	 * @see IDocument#getLineOfOffset(int)
	 */
	private int getLineOfOffset(int offset) throws BadLocationException {
		if (!isFixedWidth()) {
			return document.getLineOfOffset(offset);
		} else {
			if (offset < 0 || offset > getCharCount()) {
				throw new BadLocationException(offset + " is not a valid offset."); //$NON-NLS-1$
			}
			int widgetLine = Arrays.binarySearch(widgetLineOffsets, 0, widgetLines, offset);
			if (widgetLine < 0) {
				// no exact offset match. At this point (-widgetLine) - 1 can be used as
				// insertion point to insert the searched offset in the array. Since we do not
				// want to insert but request the line containing the offset the desired answer
				// is the index before the insertion index.
				widgetLine = (-widgetLine) - 2;
			}
			if (offset == preemptLineWrapChange) {
				// The requested offset is at fixed width border. In some text change situations
				// we must return the line index it will have after the change even if the
				// change is not applied yet. See #preemptLineWrapChange Javadoc for more
				// details.
				widgetLine--;
			}
			return widgetLine;
		}
	}

	@Override
	public int getLineCount() {
		return widgetLines;
	}

	@Override
	public String getLineDelimiter() {
		return System.lineSeparator();
	}

	@Override
	public int getOffsetAtLine(int lineIndex) {
		try {
			return getLineOffset(lineIndex);
		} catch (BadLocationException e) {
			log(e);
			return -1;
		}
	}

	/**
	 * Return the character offset of the first character of the given line.
	 * <p>
	 * Like {@link #getOffsetAtLine(int)} but throws exception in case of invalid
	 * line numbers.
	 * </p>
	 *
	 * @param widgetLineIndex the widget line number (first line has number 0)
	 * @return offset of the first character of the line
	 * @throws BadLocationException if widget line does not exist
	 * @see #getOffsetAtLine(int)
	 * @see IDocument#getLineOffset(int)
	 */
	private int getLineOffset(int widgetLineIndex) throws BadLocationException {
		if (!isFixedWidth()) {
			return document.getLineOffset(widgetLineIndex);
		} else {
			if (widgetLineIndex < 0 || widgetLineIndex >= widgetLines) {
				throw new BadLocationException(widgetLineIndex + " is not a valid line index."); //$NON-NLS-1$
			}
			return widgetLineOffsets[widgetLineIndex];
		}
	}

	@Override
	public String getTextRange(int start, int length) {
		try {
			return document.get(start, length);
		} catch (BadLocationException e) {
			log(e);
			return null;
		}
	}

	@Override
	public void replaceTextRange(int start, int replaceLength, String text) {
		try {
			document.replace(start, replaceLength, text);
		} catch (BadLocationException e) {
			log(e);
		}
	}

	@Override
	public synchronized void setText(String text) {
		document.set(text == null ? "" : text); //$NON-NLS-1$
		TextChangedEvent changeEvent = new TextChangedEvent(this);
		for (TextChangeListener listener : textChangeListeners) {
			listener.textSet(changeEvent);
		}
	}

	@Override
	public synchronized void documentAboutToBeChanged(DocumentEvent event) {
		TextChangingEvent changingEvent;
		if (!isFixedWidth()) {
			changingEvent = new TextChangingEvent(this);
			changingEvent.start = event.getOffset();
			changingEvent.newText = event.getText() == null ? "" : event.getText(); //$NON-NLS-1$
			changingEvent.replaceCharCount = event.getLength();
			changingEvent.newCharCount = changingEvent.newText.length();
			try {
				changingEvent.replaceLineCount = document.getNumberOfLines(event.getOffset(), event.getLength()) - 1;
			} catch (BadLocationException e) {
				log(e);
			}
			changingEvent.newLineCount = document.computeNumberOfLines(changingEvent.newText);
		} else {
			try {
				changingEvent = generateTextChangingEvent(event);
			} catch (BadLocationException e) {
				log(e);
				// Should never happen.
				// But provide empty changing event to hopefully reduce damage.
				changingEvent = new TextChangingEvent(this);
			}
		}

		for (TextChangeListener listener : textChangeListeners) {
			listener.textChanging(changingEvent);
		}

		if (ASSERT) {
			updatePrediction(changingEvent);
		}
	}

	/**
	 * Generate the {@link TextChangingEvent} for <b>fixed width mode</b>. Due to
	 * the dynamic wrapping of lines and the lack of line delimiters it is much more
	 * complicated than without fixed width.
	 *
	 * @param event the document change event
	 * @return the text changing event for the widget
	 * @throws BadLocationException if document event is invalid
	 */
	private TextChangingEvent generateTextChangingEvent(DocumentEvent event) throws BadLocationException {
		final String newText = event.getText() == null ? "" : event.getText(); //$NON-NLS-1$
		final int newTextLength = newText.length();
		final int eventOffset = event.getOffset();
		final int eventLength = event.getLength();
		int replaceLineCount = 0;
		int newLineCount = 0;

		// The primary duty of this method is to calculate new and removed line which
		// includes the changing in line wrapping.
		// The number of new and replaced lines must include any line whose line content
		// is changing. Normally this only includes lines directly affected by the
		// change event. But due to our magic line wrapping, as an extreme case, a
		// single character inserted at first offset can, from StyledText-Widgets
		// perspective, change the content of every line.

		if (newTextLength > 0 || eventLength > 0) {
			// In this method first and last refer to the first and last line affected by
			// the current document event
			final int eventEnd = eventOffset + eventLength;
			final int firstWidgetLineIndex = getLineOfOffset(eventOffset);
			final int firstWidgetLineOffset = getLineOffset(firstWidgetLineIndex);

			final int firstInsertLength;
			final int lastInsertLength;
			int lastDocLineLengthDiff = -eventLength;

			int newTextOffset = 0;
			Match newLineMatch = docLegalLineDelimiterMatcher.indexOf(newText, newTextOffset);
			if (newLineMatch == null) {
				// single line insert
				firstInsertLength = newTextLength;
				lastInsertLength = eventOffset - firstWidgetLineOffset + newTextLength;
				lastDocLineLengthDiff += newTextLength;
			} else {
				// multiline insert
				// processed in three parts:
				// 1. First line: everything from start of inserted text to (including) first
				// line delimiter
				// 2. Middle lines: everything from first line delimiter (exclusive) to last
				// line delimiter (inclusive) (may contain additional delimiters)
				// 3. Last line: everything (including) last line delimiter to end of inserted
				// text

				firstInsertLength = newLineMatch.getOffset();
				// newLineCount here is numbers of lines required if text is wrapped -1 because
				// we start inserting in an existing line and +1 for the first line delimiter we
				// had found
				newLineCount = linesIfWrapped(eventOffset - firstWidgetLineOffset + firstInsertLength);

				while (true) {
					newTextOffset = newLineMatch.getOffset() + newLineMatch.getText().length();
					newLineMatch = docLegalLineDelimiterMatcher.indexOf(newText, newTextOffset);
					if (newLineMatch == null) {
						break;
					}
					final int insertedLineLength = newLineMatch.getOffset() - newTextOffset;
					// new text's middle lines are unaffected from existing content and simply count
					// as number of lines they need with wrapping
					newLineCount += linesIfWrapped(insertedLineLength);
				}

				final int lastTextPartLength = newTextLength - newTextOffset;
				lastInsertLength = lastTextPartLength;
				lastDocLineLengthDiff += lastTextPartLength;
				lastDocLineLengthDiff -= eventOffset - firstWidgetLineOffset;
			}

			final int lastDocLineIndex = document.getLineOfOffset(eventEnd);
			final IRegion lastDocLine = document.getLineInformation(lastDocLineIndex);

			int affectedContentAfterRange = 0;
			if (lastDocLineLengthDiff != 0) {
				// the content after actual event range moved due to wrapping and must be
				// reported as replaced lines to StyledTextRenderer to update lines rendering
				affectedContentAfterRange = lastDocLine.getOffset() + lastDocLine.getLength() - eventEnd;
			}

			// newLineCount here is numbers of lines required if text is wrapped -1 because
			// we are prepending an existing line
			// (and no real line delimiter left to consider)
			newLineCount += linesIfWrapped(lastInsertLength + affectedContentAfterRange) - 1;

			// replaceLineCount is basically the difference between the index of the last
			// affected line (line at event offset + replace length) and the index of the
			// first affected line (line at event offset)
			// There is one special case caused by the wrapping without delimiter approach.
			// If the replace (a real replace event at this point, removing as many
			// characters as inserting) is ending at a virtual wrap border the
			// lastAffectedOffset would indicate the next line after wrap is affected even
			// if this line isn't really affected.
			final int lastAffectedOffset = eventEnd + affectedContentAfterRange;
			int lastAffectedWidgetLineIndex = getLineOfOffset(lastAffectedOffset);
			final int lastAffectedWidgetLineOffset = getLineOffset(lastAffectedWidgetLineIndex);
			if (lastAffectedWidgetLineOffset == lastAffectedOffset && lastDocLine.getOffset() != lastAffectedOffset) {
				lastAffectedWidgetLineIndex--;
			}
			replaceLineCount = lastAffectedWidgetLineIndex - firstWidgetLineIndex;

			if (firstInsertLength == 0 && eventLength > 0 && affectedContentAfterRange == 0) {
				final int firstDocLineOffset = document.getLineInformationOfOffset(eventOffset).getOffset();
				if (eventOffset != firstDocLineOffset && (eventOffset - firstDocLineOffset) % fixedConsoleWidth == 0) {
					// Text change produce a tricky wrapped line change. Change start at fixed width
					// border and is at start of wrapped line because there is wrapped content after
					// event start. After change there is no more wrapped content after so the same
					// event start offset is now one widget line above.
					replaceLineCount++;
					preemptLineWrapChange = eventOffset;
				}
			}
		}

		final TextChangingEvent changingEvent = new TextChangingEvent(this);
		changingEvent.start = eventOffset;
		changingEvent.newText = newText;
		changingEvent.replaceCharCount = eventLength;
		changingEvent.newCharCount = newTextLength;
		changingEvent.replaceLineCount = replaceLineCount;
		changingEvent.newLineCount = newLineCount;
		return changingEvent;
	}

	/**
	 * For the given text length calculate number of wrapped lines this text
	 * requires with current {@link #fixedConsoleWidth} setting.
	 * <p>
	 * A line ending at the fixed length border will not result in an extra line,
	 * i.e. a line with length of <i>consoleWidth</i> results in one line.
	 * </p>
	 * <p>
	 * Line delimiters are ignored and count like any other character. Since line
	 * delimiters should not cause line wraps this method is intended to be called
	 * with line length excluding line delimiter.
	 * </p>
	 *
	 * @param lineLength line length to calculate
	 * @return number of lines if given length is wrapped with current
	 *         {@link #fixedConsoleWidth} (always &gt;= 1)
	 */
	private int linesIfWrapped(int lineLength) {
		if (fixedConsoleWidth <= 0 || lineLength <= 0) {
			return 1;
		}
		return ((lineLength - 1) / fixedConsoleWidth) + 1;
	}

	@Override
	public synchronized void documentChanged(DocumentEvent event) {
		preemptLineWrapChange = -1;
		updateWidgetOffsets(event.getOffset());

		TextChangedEvent changeEvent = new TextChangedEvent(this);
		for (TextChangeListener listener : textChangeListeners) {
			listener.textChanged(changeEvent);
		}

		if (ASSERT) {
			verifyPrediction();
		}
	}

	/**
	 * Update list of widget line offsets.
	 * <p>
	 * <b>Note:</b> the widget line offset lookup is only used for fixed width
	 * console and therefore only updated if fixed width is enabled.
	 * </p>
	 *
	 * @param fromOffset all offsets before given offset are considered valid. Only
	 *                   update widget offsets from this offset onwards.
	 * @see #widgetLines
	 * @see #widgetLineOffsets
	 */
	private void updateWidgetOffsets(int fromOffset) {
		if (document == null) {
			widgetLines = 0;
			return;
		}

		final int docLines = document.getNumberOfLines();
		if (!isFixedWidth()) {
			widgetLines = docLines;
		} else {
			try {
				final int offset = Math.max(fromOffset, 0);
				// if someone manages to set the documents text to null the document may return
				// a negative line number
				int docLineIndex = Math.max(document.getLineOfOffset(offset), 0);
				final int docLineOffset = document.getLineOffset(docLineIndex);
				int widgetLineIndex;
				if (docLineOffset > 0) {
					widgetLineIndex = getLineOfOffset(docLineOffset);
				} else {
					widgetLineIndex = 0;
					setLookupEntry(widgetLineIndex, 0);
				}

				for (; docLineIndex < docLines; docLineIndex++) {
					int lineLength = document.getLineInformation(docLineIndex).getLength();
					for (; lineLength > fixedConsoleWidth; lineLength -= fixedConsoleWidth) {
						widgetLineIndex++;
						setLookupEntry(widgetLineIndex, widgetLineOffsets[widgetLineIndex - 1] + fixedConsoleWidth);
					}

					final String docLineDelimiter = document.getLineDelimiter(docLineIndex);
					if (docLineDelimiter != null) {
						widgetLineIndex++;
						setLookupEntry(widgetLineIndex,
								widgetLineOffsets[widgetLineIndex - 1] + lineLength + docLineDelimiter.length());
					}
				}
				widgetLines = widgetLineIndex + 1;
			} catch (BadLocationException e) {
				// should be impossible if document is not changed meanwhile
				log(e);
			}
		}
	}

	/**
	 * Set an entry in the {@link #widgetLineOffsets} lookup. Will grow the lookup
	 * array if necessary.
	 *
	 * @param widgetLineIndex the lookup entry to set (does not have to exist yet)
	 * @param value           the entry value to set
	 */
	private void setLookupEntry(int widgetLineIndex, int value) {
		ensureOffsetsCapacity(widgetLineIndex + 1);
		widgetLineOffsets[widgetLineIndex] = value;
	}

	/**
	 * Ensure the offset lookup array can store at least <i>size</i> entries.
	 *
	 * @param requiredSize minimum size lookup array should have after
	 * @see #widgetLineOffsets
	 */
	private void ensureOffsetsCapacity(int requiredSize) {
		final int oldSize = widgetLineOffsets != null ? widgetLineOffsets.length : 0;
		if (oldSize < requiredSize) {
			final int[] oldWidgetOffsets = widgetLineOffsets;
			widgetLineOffsets = new int[requiredSize + GROW];
			if (oldSize > 0) {
				System.arraycopy(oldWidgetOffsets, 0, widgetLineOffsets, 0, oldSize);
			}
		}
	}

	/**
	 * Check if fixed width console feature is enabled or not.
	 *
	 * @return true if lines are wrapped at fixed width
	 * @see #getWidth()
	 */
	public boolean isFixedWidth() {
		return fixedConsoleWidth > 0;
	}

	/**
	 * Get current consoles fixed width.
	 *
	 * @return current fixed console width or &lt;= 0 if disabled
	 * @see #isFixedWidth()
	 */
	public int getWidth() {
		return fixedConsoleWidth;
	}

	/**
	 * Set new fixed console width. Also signals text viewer widget to render
	 * content with new fixed width.
	 *
	 * @param width the fixed console width or &lt;= 0 to not break lines at fixed
	 *              width
	 */
	public void setWidth(int width) {
		if (width != fixedConsoleWidth) {
			fixedConsoleWidth = width;
			updateWidgetOffsets(0);
			TextChangedEvent changeEvent = new TextChangedEvent(this);
			for (TextChangeListener listener : textChangeListeners) {
				listener.textSet(changeEvent);
			}
		}
	}

	/**
	 * Log an exception and include if error occurred in fixed or non fixed width
	 * mode.
	 *
	 * @param error the error to log
	 */
	private void log(Throwable error) {
		ConsolePlugin.log(ConsolePlugin.newErrorStatus("fixed width: " + isFixedWidth(), error)); //$NON-NLS-1$
	}

	// +---------------------+
	// | Debug and test code |
	// +---------------------+
	/**
	 * The expected document length after next document change is applied. Only used
	 * if {@link #ASSERT} is <code>true</code>.
	 */
	private int predictedCharCount;
	/**
	 * The expected number of lines after next document change is applied. Only used
	 * if {@link #ASSERT} is <code>true</code>.
	 */
	private int predictedLines;

	/**
	 * Set the expected document length and lines from the current document state
	 * and the changes predicted by the changing event.
	 *
	 * @param event the {@link TextChangingEvent} describing the next document
	 *              change
	 */
	private void updatePrediction(TextChangingEvent event) {
		predictedCharCount = getCharCount() + event.newCharCount - event.replaceCharCount;
		predictedLines = getLineCount() + event.newLineCount - event.replaceLineCount;
	}

	/**
	 * Check if the last change prediction was correct. Throws an
	 * AssertionFailedException if the prediction was wrong.
	 */
	private void verifyPrediction() {
		final int charCount = getCharCount();
		Assert.isTrue(predictedCharCount == charCount, String.format(java.util.Locale.ROOT,
				"Wrong char count. Expected<%d>, Actual<%d>", predictedCharCount, charCount)); //$NON-NLS-1$
		final int lineCount = getLineCount();
		Assert.isTrue(predictedLines == lineCount, String.format(java.util.Locale.ROOT,
				"Wrong line count. Expected<%d>, Actual<%d>", predictedLines, lineCount)); //$NON-NLS-1$
	}
}