1
0
mirror of https://github.com/SKCraft/Launcher.git synced 2024-11-24 12:16:28 +01:00

Merge pull request #82 from seebs/master

Avoid pathological failure mode when trimming lines.
This commit is contained in:
sk89q 2015-08-03 13:40:54 -07:00
commit 40555cce59
2 changed files with 45 additions and 27 deletions

View File

@ -111,21 +111,29 @@ public class MessageLog extends JPanel {
* @param line line * @param line line
* @param attributes attribute set, or null for none * @param attributes attribute set, or null for none
*/ */
public void log(String line, AttributeSet attributes) { public void log(final String line, AttributeSet attributes) {
final Document d = document;
final JTextComponent t = textComponent;
if (colorEnabled) { if (colorEnabled) {
if (line.startsWith("(!!)")) { if (line.startsWith("(!!)")) {
attributes = highlightedAttributes; attributes = highlightedAttributes;
} }
} }
final AttributeSet a = attributes;
try { SwingUtilities.invokeLater(new Runnable() {
int offset = document.getLength(); @Override
document.insertString(offset, line, public void run() {
(attributes != null && colorEnabled) ? attributes : defaultAttributes); try {
textComponent.setCaretPosition(document.getLength()); int offset = d.getLength();
} catch (BadLocationException ble) { d.insertString(offset, line,
(a != null && colorEnabled) ? a : defaultAttributes);
t.setCaretPosition(d.getLength());
} catch (BadLocationException ble) {
} }
}
});
} }
/** /**

View File

@ -21,6 +21,7 @@ import javax.swing.text.Element;
public class LimitLinesDocumentListener implements DocumentListener { public class LimitLinesDocumentListener implements DocumentListener {
private int maximumLines; private int maximumLines;
private boolean isRemoveFromStart; private boolean isRemoveFromStart;
private volatile boolean isRemoving;
/** /**
* Specify the number of lines to be stored in the Document. Extra lines * Specify the number of lines to be stored in the Document. Extra lines
@ -34,6 +35,7 @@ public class LimitLinesDocumentListener implements DocumentListener {
boolean isRemoveFromStart) { boolean isRemoveFromStart) {
setLimitLines(maximumLines); setLimitLines(maximumLines);
this.isRemoveFromStart = isRemoveFromStart; this.isRemoveFromStart = isRemoveFromStart;
this.isRemoving = false;
} }
/** /**
@ -54,12 +56,15 @@ public class LimitLinesDocumentListener implements DocumentListener {
// Changes to the Document can not be done within the listener // Changes to the Document can not be done within the listener
// so we need to add the processing to the end of the EDT // so we need to add the processing to the end of the EDT
SwingUtilities.invokeLater(new Runnable() { if (!this.isRemoving) {
@Override this.isRemoving = true;
public void run() { SwingUtilities.invokeLater(new Runnable() {
removeLines(e); @Override
} public void run() {
}); removeLines(e);
}
});
}
} }
@Override @Override
@ -74,20 +79,25 @@ public class LimitLinesDocumentListener implements DocumentListener {
// The root Element of the Document will tell us the total number // The root Element of the Document will tell us the total number
// of line in the Document. // of line in the Document.
Document document = e.getDocument(); try {
Element root = document.getDefaultRootElement(); Document document = e.getDocument();
Element root = document.getDefaultRootElement();
int excess = root.getElementCount() - maximumLines;
while (root.getElementCount() > maximumLines) { if (excess > 0) {
if (isRemoveFromStart) { if (isRemoveFromStart) {
removeFromStart(document, root); removeFromStart(document, root, excess);
} else { } else {
removeFromEnd(document, root); removeFromEnd(document, root);
}
} }
} finally {
this.isRemoving = false;
} }
} }
private void removeFromStart(Document document, Element root) { private void removeFromStart(Document document, Element root, int excess) {
Element line = root.getElement(0); Element line = root.getElement(excess - 1);
int end = line.getEndOffset(); int end = line.getEndOffset();
try { try {
@ -101,9 +111,9 @@ public class LimitLinesDocumentListener implements DocumentListener {
// We use start minus 1 to make sure we remove the newline // We use start minus 1 to make sure we remove the newline
// character of the previous line // character of the previous line
Element line = root.getElement(root.getElementCount() - 1); Element line = root.getElement(maximumLines);
int start = line.getStartOffset(); int start = line.getStartOffset();
int end = line.getEndOffset(); int end = root.getEndOffset();
try { try {
document.remove(start - 1, end - start); document.remove(start - 1, end - start);