diff options
author | Philippe Marschall | 2014-12-19 12:30:49 +0000 |
---|---|---|
committer | Michael Rennie | 2015-03-05 16:55:57 +0000 |
commit | 84f42b7ba42b87423f99d3e2e991d2e59c04de4d (patch) | |
tree | b5a2dadbb80e607d7fb3d27c530510911d169035 | |
parent | 4033dafbeb0b55279a16ddab06d8db5e397f7bb2 (diff) | |
download | eclipse.platform.debug-84f42b7ba42b87423f99d3e2e991d2e59c04de4d.tar.gz eclipse.platform.debug-84f42b7ba42b87423f99d3e2e991d2e59c04de4d.tar.xz eclipse.platform.debug-84f42b7ba42b87423f99d3e2e991d2e59c04de4d.zip |
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. Updated change "\r\n" is no longer considered a sequence of control
characters.
Change-Id: I93f394a44fcdd891a6e139c7c055c67313187e0e
Signed-off-by: Philippe Marschall <philippe.marschall@netcetera.ch>
-rw-r--r-- | org.eclipse.ui.console/src/org/eclipse/ui/internal/console/ConsoleDocument.java | 148 |
1 files changed, 147 insertions, 1 deletions
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 8eb24bb79..2be213198 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,24 @@ import org.eclipse.jface.text.Position; */ public class ConsoleDocument extends Document { + private static final char NEW_LINE = '\n'; + + 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 +108,51 @@ public class ConsoleDocument extends Document { */ @Override public synchronized void replace(int pos, int length, String text) throws BadLocationException { - super.replace(pos, length, text); + if (containsControlCharacter(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 +190,87 @@ public class ConsoleDocument extends Document { public synchronized Position[] getPositions(String category) throws BadPositionCategoryException { return super.getPositions(category); } + + private static boolean containsControlCharacter(String text) { + int length = text.length(); + int i = 0; + while (i < length) { + char ch = text.charAt(i); + if (ch == BACK_SPACE || ch == FORM_FEED) { + return true; + } + if (ch == CARRIAGE_RETURN) { + if (i + 1 < length && text.charAt(i + 1) == NEW_LINE) { + // don't treat CR LF on Windows as control character + // skip the character after the current one since we already + // know it's a newline + i += 2; + continue; + } + return true; + } + i += 1; + } + 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; + } } |