1
0
mirror of https://github.com/arduino/Arduino.git synced 2025-02-18 12:54:25 +01:00

Slightly improved how EditorConsole works

This commit is contained in:
Federico Fissore 2015-10-30 15:31:58 +01:00
parent c7cb263cf0
commit e5252e3031
2 changed files with 23 additions and 20 deletions

View File

@ -40,7 +40,6 @@ import processing.app.EditorConsole;
import javax.swing.*; import javax.swing.*;
import javax.swing.text.BadLocationException; import javax.swing.text.BadLocationException;
import javax.swing.text.Document;
import javax.swing.text.SimpleAttributeSet; import javax.swing.text.SimpleAttributeSet;
import java.io.ByteArrayOutputStream; import java.io.ByteArrayOutputStream;
import java.io.PrintStream; import java.io.PrintStream;
@ -57,8 +56,7 @@ public class ConsoleOutputStream extends ByteArrayOutputStream {
private final PrintStream printStream; private final PrintStream printStream;
private final StringBuilder buffer; private final StringBuilder buffer;
private final Timer timer; private final Timer timer;
private JScrollPane scrollPane; private volatile EditorConsole editorConsole;
private Document document;
public ConsoleOutputStream(SimpleAttributeSet attributes, PrintStream printStream) { public ConsoleOutputStream(SimpleAttributeSet attributes, PrintStream printStream) {
this.attributes = attributes; this.attributes = attributes;
@ -66,19 +64,15 @@ public class ConsoleOutputStream extends ByteArrayOutputStream {
this.buffer = new StringBuilder(); this.buffer = new StringBuilder();
this.timer = new Timer(100, (e) -> { this.timer = new Timer(100, (e) -> {
if (scrollPane != null) { if (editorConsole != null) {
synchronized (scrollPane) { editorConsole.scrollDown();
scrollPane.getHorizontalScrollBar().setValue(0);
scrollPane.getVerticalScrollBar().setValue(scrollPane.getVerticalScrollBar().getMaximum());
}
} }
}); });
timer.setRepeats(false); timer.setRepeats(false);
} }
public synchronized void setCurrentEditorConsole(EditorConsole console) { public void setCurrentEditorConsole(EditorConsole console) {
this.scrollPane = console; this.editorConsole = console;
this.document = console.getDocument();
} }
public synchronized void flush() { public synchronized void flush() {
@ -102,7 +96,7 @@ public class ConsoleOutputStream extends ByteArrayOutputStream {
} }
private void resetBufferIfDocumentEmpty() { private void resetBufferIfDocumentEmpty() {
if (document != null && document.getLength() == 0) { if (editorConsole != null && editorConsole.isEmpty()) {
buffer.setLength(0); buffer.setLength(0);
} }
} }
@ -113,12 +107,10 @@ public class ConsoleOutputStream extends ByteArrayOutputStream {
printStream.print(line); printStream.print(line);
if (document != null) { if (editorConsole != null) {
SwingUtilities.invokeLater(() -> { SwingUtilities.invokeLater(() -> {
try { try {
String lineWithoutCR = line.replace("\r\n", "\n").replace("\r", "\n"); editorConsole.insertString(line, attributes);
int offset = document.getLength();
document.insertString(offset, lineWithoutCR, attributes);
} catch (BadLocationException ble) { } catch (BadLocationException ble) {
//ignore //ignore
} }

View File

@ -36,7 +36,7 @@ public class EditorConsole extends JScrollPane {
private static ConsoleOutputStream out; private static ConsoleOutputStream out;
private static ConsoleOutputStream err; private static ConsoleOutputStream err;
public static synchronized void init(SimpleAttributeSet outStyle, PrintStream outStream, SimpleAttributeSet errStyle, PrintStream errStream) { private static synchronized void init(SimpleAttributeSet outStyle, PrintStream outStream, SimpleAttributeSet errStyle, PrintStream errStream) {
if (out != null) { if (out != null) {
return; return;
} }
@ -116,11 +116,22 @@ public class EditorConsole extends JScrollPane {
} }
} }
public void scrollDown() {
getHorizontalScrollBar().setValue(0);
getVerticalScrollBar().setValue(getVerticalScrollBar().getMaximum());
}
public boolean isEmpty() {
return document.getLength() == 0;
}
public void insertString(String line, SimpleAttributeSet attributes) throws BadLocationException {
int offset = document.getLength();
document.insertString(offset, line, attributes);
}
public String getText() { public String getText() {
return consoleTextPane.getText().trim(); return consoleTextPane.getText().trim();
} }
public Document getDocument() {
return document;
}
} }