MDS/openide
1
0
Fork 0
mirror of https://gitflic.ru/project/openide/openide.git synced 2026-09-27 10:03:11 +07:00
Code Issues Packages Projects Releases Wiki Activity

simplify for IDEA-CR-42198

Browse Source
This commit is contained in:
Alexey Kudravtsev
2019-01-17 15:26:24 +03:00
parent 289f29a931
commit 6645fde04a
1 changed files with 24 additions and 41 deletions
Download Patch File Download Diff File Expand all files Collapse all files
platform/lang-impl/src/com/intellij/execution/impl/ConsoleViewImpl.java
+24 -41
View File
@@ -775,62 +775,45 @@ public class ConsoleViewImpl extends JPanel implements ConsoleView, ObservableCo
return prefix;
}
// convert all "a\bc" sequences to "c", not crossing the line boundaries in the process
private static void normalizeBackspaceCharacters(@NotNull StringBuilder text) {
int ind = StringUtil.indexOf(text, BACKSPACE);
if (ind < 0) {
return;
}
int i = 0;
int guardLength = 0;
int oldLength = text.length();
int newLength = 0;
while (i < oldLength) {
LineSeparator lineSeparator = StringUtil.getLineSeparatorAt(text, i);
if (lineSeparator != null) {
int sepLength = lineSeparator.getSeparatorString().length();
copyString(lineSeparator.getSeparatorString(), sepLength, text, newLength);
newLength += sepLength;
guardLength = newLength;
i += sepLength;
}
else {
char ch = text.charAt(i);
final boolean append;
if (ch == BACKSPACE) {
assert guardLength <= newLength;
if (guardLength == newLength) {
// Backspace is the first char in a new line:
// Keep backspace at the first line (guardLength == 0) as it might be in the middle of the actual line,
// handle it later (see getBackspacePrefixLength).
// Otherwise (for non-first lines), skip backspace as it can't be interpreted if located right after line ending.
append = guardLength == 0;
}
else {
append = text.charAt(newLength - 1) == BACKSPACE;
if (!append) {
newLength--; // interpret \b: delete prev char
}
}
for (int i = 0; i < text.length(); i++) {
char ch = text.charAt(i);
final boolean append;
if (ch == BACKSPACE) {
assert guardLength <= newLength;
if (guardLength == newLength) {
// Backspace is the first char in a new line:
// Keep backspace at the first line (guardLength == 0) as it might be in the middle of the actual line,
// handle it later (see getBackspacePrefixLength).
// Otherwise (for non-first lines), skip backspace as it can't be interpreted if located right after line ending.
append = guardLength == 0;
}
else {
append = true;
append = text.charAt(newLength - 1) == BACKSPACE;
if (!append) {
newLength--; // interpret \b: delete prev char
}
}
if (append) {
text.setCharAt(newLength, ch);
newLength++;
}
i++;
}
else {
append = true;
}
if (append) {
text.setCharAt(newLength, ch);
newLength++;
if (ch == '\r' || ch == '\n') guardLength = newLength;
}
}
text.setLength(newLength);
}
private static void copyString(@NotNull String src, int srcCount, @NotNull StringBuilder dest, int destStartOffset) {
for (int i = 0; i < srcCount; i++) {
dest.setCharAt(destStartOffset + i, src.charAt(i));
}
}
private void createTokenRangeHighlighter(@NotNull ConsoleViewContentType contentType,
int startOffset,
int endOffset) {