rooty/Arduino
1
0
Fork 0
mirror of https://github.com/arduino/Arduino.git synced 2025-02-26 20:54:22 +01:00
Code Issues Releases Activity

Apply on-the-fly setFontSize to Console

Browse Source 
Fixes #7022
This commit is contained in:
Martino Facchin 2017-12-15 12:38:24 +01:00
parent 4aec8997e2
commit b6280cfd65
3 changed files with 25 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
app/src/cc/arduino/ConsoleOutputStream.java
View File

@ -52,7 +52,7 @@ import java.io.PrintStream;
*/ */
public class ConsoleOutputStream extends ByteArrayOutputStream { public class ConsoleOutputStream extends ByteArrayOutputStream {
private final SimpleAttributeSet attributes; private SimpleAttributeSet attributes;
private final PrintStream printStream; private final PrintStream printStream;
private final Timer timer; private final Timer timer;
@ -73,6 +73,10 @@ public class ConsoleOutputStream extends ByteArrayOutputStream {
timer.setRepeats(false); timer.setRepeats(false);
} }
public void setAttibutes(SimpleAttributeSet attributes) {
this.attributes = attributes;
}
public void setCurrentEditorConsole(EditorConsole console) { public void setCurrentEditorConsole(EditorConsole console) {
this.editorConsole = console; this.editorConsole = console;
} }

4
app/src/processing/app/Editor.java
View File

@ -458,9 +458,11 @@ public class Editor extends JFrame implements RunnerListener {
boolean external = PreferencesData.getBoolean("editor.external"); boolean external = PreferencesData.getBoolean("editor.external");
saveMenuItem.setEnabled(!external); saveMenuItem.setEnabled(!external);
saveAsMenuItem.setEnabled(!external); saveAsMenuItem.setEnabled(!external);
for (EditorTab tab: tabs) for (EditorTab tab: tabs) {
tab.applyPreferences(); tab.applyPreferences();
} }
console.applyPreferences();
}
// . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . // . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

19
app/src/processing/app/EditorConsole.java
View File

@ -58,6 +58,9 @@ public class EditorConsole extends JScrollPane {
private final DefaultStyledDocument document; private final DefaultStyledDocument document;
private final JTextPane consoleTextPane; private final JTextPane consoleTextPane;
private SimpleAttributeSet stdOutStyle;
private SimpleAttributeSet stdErrStyle;
public EditorConsole() { public EditorConsole() {
document = new DefaultStyledDocument(); document = new DefaultStyledDocument();
@ -74,7 +77,7 @@ public class EditorConsole extends JScrollPane {
Font editorFont = PreferencesData.getFont("editor.font"); Font editorFont = PreferencesData.getFont("editor.font");
Font actualFont = new Font(consoleFont.getName(), consoleFont.getStyle(), scale(editorFont.getSize())); Font actualFont = new Font(consoleFont.getName(), consoleFont.getStyle(), scale(editorFont.getSize()));
SimpleAttributeSet stdOutStyle = new SimpleAttributeSet(); stdOutStyle = new SimpleAttributeSet();
StyleConstants.setForeground(stdOutStyle, Theme.getColor("console.output.color")); StyleConstants.setForeground(stdOutStyle, Theme.getColor("console.output.color"));
StyleConstants.setBackground(stdOutStyle, backgroundColour); StyleConstants.setBackground(stdOutStyle, backgroundColour);
StyleConstants.setFontSize(stdOutStyle, actualFont.getSize()); StyleConstants.setFontSize(stdOutStyle, actualFont.getSize());
@ -84,7 +87,7 @@ public class EditorConsole extends JScrollPane {
consoleTextPane.setParagraphAttributes(stdOutStyle, true); consoleTextPane.setParagraphAttributes(stdOutStyle, true);
SimpleAttributeSet stdErrStyle = new SimpleAttributeSet(); stdErrStyle = new SimpleAttributeSet();
StyleConstants.setForeground(stdErrStyle, Theme.getColor("console.error.color")); StyleConstants.setForeground(stdErrStyle, Theme.getColor("console.error.color"));
StyleConstants.setBackground(stdErrStyle, backgroundColour); StyleConstants.setBackground(stdErrStyle, backgroundColour);
StyleConstants.setFontSize(stdErrStyle, actualFont.getSize()); StyleConstants.setFontSize(stdErrStyle, actualFont.getSize());
@ -109,6 +112,18 @@ public class EditorConsole extends JScrollPane {
EditorConsole.init(stdOutStyle, System.out, stdErrStyle, System.err); EditorConsole.init(stdOutStyle, System.out, stdErrStyle, System.err);
} }
public void applyPreferences() {
Font consoleFont = Theme.getFont("console.font");
Font editorFont = PreferencesData.getFont("editor.font");
Font actualFont = new Font(consoleFont.getName(), consoleFont.getStyle(), scale(editorFont.getSize()));
StyleConstants.setFontSize(stdOutStyle, actualFont.getSize());
StyleConstants.setFontSize(stdErrStyle, actualFont.getSize());
out.setAttibutes(stdOutStyle);
err.setAttibutes(stdErrStyle);
}
public void clear() { public void clear() {
try { try {
document.remove(0, document.getLength()); document.remove(0, document.getLength());