Bug 76936 - [console] Eclipse Console window does not handle \b, \f, and
\r
Change ConsoleDocument to process the text String to handle \b, \f, and
\r.
Change-Id: I2071ea53fc521a0acc5e4e6ffec9aab0b1af21ea
Signed-off-by: Philippe Marschall <philippe.marschall@netcetera.ch>
diff --git a/org.eclipse.ui.console/src/org/eclipse/ui/internal/console/ConsoleDocument.java b/org.eclipse.ui.console/src/org/eclipse/ui/internal/console/ConsoleDocument.java
index 8eb24bb..7c1e1f9 100644
--- a/org.eclipse.ui.console/src/org/eclipse/ui/internal/console/ConsoleDocument.java
+++ b/org.eclipse.ui.console/src/org/eclipse/ui/internal/console/ConsoleDocument.java
@@ -7,6 +7,7 @@
*
* Contributors:
* IBM Corporation - initial API and implementation
+ * Philippe Marschall <philippe.marschall@netcetera.ch> - Bug 76936
*******************************************************************************/
package org.eclipse.ui.internal.console;
@@ -21,6 +22,22 @@
*/
public class ConsoleDocument extends Document {
+ private static final char BACK_SPACE = '\b';
+
+ private static final char CARRIAGE_RETURN = '\r';
+
+ private static final char FORM_FEED = '\f';
+
+ static final class DelimiterInfo {
+ int delimiterIndex;
+ int delimiterLength;
+
+ DelimiterInfo(int delimiterIndex, int delimiterLength) {
+ this.delimiterIndex = delimiterIndex;
+ this.delimiterLength = delimiterLength;
+ }
+ }
+
/* (non-Javadoc)
* @see org.eclipse.jface.text.IDocument#get(int, int)
*/
@@ -89,7 +106,51 @@
*/
@Override
public synchronized void replace(int pos, int length, String text) throws BadLocationException {
- super.replace(pos, length, text);
+ if (containsBacktrackCharacter(text)) {
+ int lineNumber = this.getTracker().getLineNumberOfOffset(pos);
+ boolean endsWithNewLIne = getLineDelimiter(lineNumber) != null;
+ int actualPosition;
+ StringBuilder buffer;
+ int lengthDelta;
+ if (endsWithNewLIne) {
+ // pos is the start of a new line
+ // assume form feeds are rare and therefore don't add additional
+ // capacity
+ buffer = new StringBuilder(length);
+ actualPosition = pos;
+ lengthDelta = 0;
+ } else {
+ // there already exists a line which we may have to modify
+ IRegion lineInformation = getLineInformation(lineNumber);
+ actualPosition = lineInformation.getOffset();
+ // assume form feeds are rare and therefore don't add additional
+ // capacity
+ int lineLength = lineInformation.getLength();
+ buffer = new StringBuilder(length + lineLength);
+ String line = get(lineInformation.getOffset(), lineLength);
+ buffer.append(line);
+ lengthDelta = lineLength;
+ }
+
+ int offset = 0;
+ int lineStart = 0; // start of the current line in the output buffer
+ DelimiterInfo delimiterInfo = nextDelimiterInfo(text, offset);
+ while (delimiterInfo != null) {
+ processLine(text, offset, lineStart, delimiterInfo.delimiterIndex - offset, buffer);
+ buffer.append(text, delimiterInfo.delimiterIndex, delimiterInfo.delimiterIndex + delimiterInfo.delimiterLength);
+
+ offset = delimiterInfo.delimiterIndex + delimiterInfo.delimiterLength;
+ delimiterInfo = nextDelimiterInfo(text, offset);
+ lineStart = buffer.length();
+
+ }
+ processLine(text, offset, lineStart, text.length() - offset, buffer);
+
+ String processedText = buffer.toString();
+ super.replace(actualPosition, length + lengthDelta, processedText);
+ } else {
+ super.replace(pos, length, text);
+ }
}
/* (non-Javadoc)
* @see org.eclipse.jface.text.IDocument#set(java.lang.String)
@@ -127,4 +188,75 @@
public synchronized Position[] getPositions(String category) throws BadPositionCategoryException {
return super.getPositions(category);
}
+
+ private static boolean containsBacktrackCharacter(String text) {
+ int length = text.length();
+ for (int i = 0; i < length; i++) {
+ char ch = text.charAt(i);
+ if (ch == BACK_SPACE || ch == CARRIAGE_RETURN || ch == FORM_FEED) {
+ return true;
+ }
+ }
+ return false;
+ }
+
+ private static void processLine(String text, int start, int initialLineStart, int length, StringBuilder buffer) {
+ if (length == 0) {
+ return;
+ }
+
+ // position where the next character insert should happen
+ int insertIndex = buffer.length();
+ // start index of the current line in the output buffer
+ int lineStart = initialLineStart;
+ // end index of the line in text
+ int end = start + length;
+ for (int i = start; i < end; i++) {
+ char ch = text.charAt(i);
+ if (ch == BACK_SPACE) {
+ if (insertIndex > lineStart) {
+ // can backtrack only in current line
+ insertIndex -= 1;
+ }
+ } else if (ch == CARRIAGE_RETURN) {
+ insertIndex = lineStart;
+ } else if (ch == FORM_FEED) {
+ int headPosition = insertIndex - lineStart;
+ buffer.append('\n');
+ lineStart = buffer.length();
+ for (int j = 0; j < headPosition; j++) {
+ buffer.append(' ');
+ }
+ insertIndex = lineStart + headPosition;
+ } else {
+ // other character insert at insertIndex
+ if (insertIndex == buffer.length()) {
+ buffer.append(ch);
+ } else {
+ // #charAt does not work when index == length
+ buffer.setCharAt(insertIndex, ch);
+ }
+ insertIndex += 1;
+ }
+ }
+ }
+
+ private static DelimiterInfo nextDelimiterInfo(String text, int offset) {
+ int length = text.length();
+ for (int i = offset; i < length; i++) {
+ char ch = text.charAt(i);
+ if (ch == '\r') {
+ // \r\n -> will be treated as a new line
+ // \r something else -> will be treated as \r
+ if (i + 1 < length) {
+ if (text.charAt(i + 1) == '\n') {
+ return new DelimiterInfo(i, 2);
+ }
+ }
+ } else if (ch == '\n') {
+ return new DelimiterInfo(i, 1);
+ }
+ }
+ return null;
+ }
}
