From b6280cfd6542fe1cc97e2b368be84a8951410aca Mon Sep 17 00:00:00 2001
From: Martino Facchin <m.facchin@arduino.cc>
Date: Fri, 15 Dec 2017 12:38:24 +0100
Subject: [PATCH] Apply on-the-fly setFontSize to Console

Fixes #7022
---
 app/src/cc/arduino/ConsoleOutputStream.java |  6 +++++-
 app/src/processing/app/Editor.java          |  4 +++-
 app/src/processing/app/EditorConsole.java   | 19 +++++++++++++++++--
 3 files changed, 25 insertions(+), 4 deletions(-)

diff --git a/app/src/cc/arduino/ConsoleOutputStream.java b/app/src/cc/arduino/ConsoleOutputStream.java
index 452c190b4..6334f11e7 100644
--- a/app/src/cc/arduino/ConsoleOutputStream.java
+++ b/app/src/cc/arduino/ConsoleOutputStream.java
@@ -52,7 +52,7 @@ import java.io.PrintStream;
  */
 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 class ConsoleOutputStream extends ByteArrayOutputStream {
     timer.setRepeats(false);
   }
 
+  public void setAttibutes(SimpleAttributeSet attributes) {
+    this.attributes = attributes;
+  }
+
   public void setCurrentEditorConsole(EditorConsole console) {
     this.editorConsole = console;
   }
diff --git a/app/src/processing/app/Editor.java b/app/src/processing/app/Editor.java
index 4d12a58b0..e2918efcd 100644
--- a/app/src/processing/app/Editor.java
+++ b/app/src/processing/app/Editor.java
@@ -458,8 +458,10 @@ public class Editor extends JFrame implements RunnerListener {
     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 --git a/app/src/processing/app/EditorConsole.java b/app/src/processing/app/EditorConsole.java
index b32382354..f656798f0 100644
--- a/app/src/processing/app/EditorConsole.java
+++ b/app/src/processing/app/EditorConsole.java
@@ -58,6 +58,9 @@ public class EditorConsole extends JScrollPane {
   private final DefaultStyledDocument document;
   private final JTextPane consoleTextPane;
 
+  private SimpleAttributeSet stdOutStyle;
+  private SimpleAttributeSet stdErrStyle;
+
   public EditorConsole() {
     document = new DefaultStyledDocument();
 
@@ -74,7 +77,7 @@ public class EditorConsole extends JScrollPane {
     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 class EditorConsole extends JScrollPane {
 
     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 class EditorConsole extends JScrollPane {
     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());