Apply on-the-fly setFontSize to Console

Fixes #7022

Author: facchinm

Diff for: app/src/cc/arduino/ConsoleOutputStream.java

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

Diff for: app/src/processing/app/Editor.java

@@ -480,8 +480,10 @@ public void applyPreferences() {
     boolean external = PreferencesData.getBoolean("editor.external");
     saveMenuItem.setEnabled(!external);
     saveAsMenuItem.setEnabled(!external);
-    for (EditorTab tab: tabs)
+    for (EditorTab tab: tabs) {
       tab.applyPreferences();
+    }
+    console.applyPreferences();
   }
 
 

Diff for: app/src/processing/app/EditorConsole.java

@@ -58,6 +58,9 @@ public static void setCurrentEditorConsole(EditorConsole console) {
   private final DefaultStyledDocument document;
   private final JTextPane consoleTextPane;
 
+  private SimpleAttributeSet stdOutStyle;
+  private SimpleAttributeSet stdErrStyle;
+
   public EditorConsole() {
     document = new DefaultStyledDocument();
 
@@ -74,7 +77,7 @@ public EditorConsole() {
     Font editorFont = PreferencesData.getFont("editor.font");
     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.setBackground(stdOutStyle, backgroundColour);
     StyleConstants.setFontSize(stdOutStyle, actualFont.getSize());
@@ -84,7 +87,7 @@ public EditorConsole() {
 
     consoleTextPane.setParagraphAttributes(stdOutStyle, true);
 
-    SimpleAttributeSet stdErrStyle = new SimpleAttributeSet();
+    stdErrStyle = new SimpleAttributeSet();
     StyleConstants.setForeground(stdErrStyle, Theme.getColor("console.error.color"));
     StyleConstants.setBackground(stdErrStyle, backgroundColour);
     StyleConstants.setFontSize(stdErrStyle, actualFont.getSize());
@@ -109,6 +112,18 @@ public EditorConsole() {
     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() {
     try {
       document.remove(0, document.getLength());