From 4659c6f9852e3f6ce329645c8fb31d5b6bc9a8f2 Mon Sep 17 00:00:00 2001 From: Cristian Maglie Date: Sun, 17 Jan 2016 11:36:42 +0200 Subject: [PATCH] Auto-scale editor and console fonts as well --- app/src/processing/app/Editor.java | 7 +++---- app/src/processing/app/EditorConsole.java | 4 +++- app/src/processing/app/Theme.java | 8 ++++++++ 3 files changed, 14 insertions(+), 5 deletions(-) diff --git a/app/src/processing/app/Editor.java b/app/src/processing/app/Editor.java index f77d80795..b645a4d50 100644 --- a/app/src/processing/app/Editor.java +++ b/app/src/processing/app/Editor.java @@ -503,10 +503,9 @@ public class Editor extends JFrame implements RunnerListener { } // apply changes to the font size for the editor - //TextAreaPainter painter = textarea.getPainter(); - textarea.setFont(PreferencesData.getFont("editor.font")); - //Font font = painter.getFont(); - //textarea.getPainter().setFont(new Font("Courier", Font.PLAIN, 36)); + Font editorFont = scale(PreferencesData.getFont("editor.font")); + textarea.setFont(editorFont); + scrollPane.getGutter().setLineNumberFont(editorFont); // in case tab expansion stuff has changed // listener.applyPreferences(); diff --git a/app/src/processing/app/EditorConsole.java b/app/src/processing/app/EditorConsole.java index f31a01b00..686fb9014 100644 --- a/app/src/processing/app/EditorConsole.java +++ b/app/src/processing/app/EditorConsole.java @@ -28,6 +28,8 @@ import javax.swing.text.*; import java.awt.*; import java.io.PrintStream; +import static processing.app.Theme.scale; + /** * Message console that sits below the editing area. */ @@ -70,7 +72,7 @@ public class EditorConsole extends JScrollPane { Font consoleFont = Theme.getFont("console.font"); Font editorFont = PreferencesData.getFont("editor.font"); - Font actualFont = new Font(consoleFont.getName(), consoleFont.getStyle(), editorFont.getSize()); + Font actualFont = new Font(consoleFont.getName(), consoleFont.getStyle(), scale(editorFont.getSize())); SimpleAttributeSet stdOutStyle = new SimpleAttributeSet(); StyleConstants.setForeground(stdOutStyle, Theme.getColor("console.output.color")); diff --git a/app/src/processing/app/Theme.java b/app/src/processing/app/Theme.java index c42e5396f..931710342 100644 --- a/app/src/processing/app/Theme.java +++ b/app/src/processing/app/Theme.java @@ -133,6 +133,14 @@ public class Theme { return new Dimension(scale(dim.width), scale(dim.height)); } + static public Font scale(Font font) { + float size = scale(font.getSize()); + // size must be float to call the correct Font.deriveFont(float) + // method that is different from Font.deriveFont(int)! + Font scaled = font.deriveFont(size); + return scaled; + } + static public Rectangle scale(Rectangle rect) { Rectangle res = new Rectangle(rect); res.x = scale(res.x);