File tree 3 files changed +14
-5
lines changed
3 files changed +14
-5
lines changed Original file line number Diff line number Diff line change @@ -503,10 +503,9 @@ public void applyPreferences() {
503
503
}
504
504
505
505
// apply changes to the font size for the editor
506
- //TextAreaPainter painter = textarea.getPainter();
507
- textarea .setFont (PreferencesData .getFont ("editor.font" ));
508
- //Font font = painter.getFont();
509
- //textarea.getPainter().setFont(new Font("Courier", Font.PLAIN, 36));
506
+ Font editorFont = scale (PreferencesData .getFont ("editor.font" ));
507
+ textarea .setFont (editorFont );
508
+ scrollPane .getGutter ().setLineNumberFont (editorFont );
510
509
511
510
// in case tab expansion stuff has changed
512
511
// listener.applyPreferences();
Original file line number Diff line number Diff line change 28
28
import java .awt .*;
29
29
import java .io .PrintStream ;
30
30
31
+ import static processing .app .Theme .scale ;
32
+
31
33
/**
32
34
* Message console that sits below the editing area.
33
35
*/
@@ -70,7 +72,7 @@ public EditorConsole() {
70
72
71
73
Font consoleFont = Theme .getFont ("console.font" );
72
74
Font editorFont = PreferencesData .getFont ("editor.font" );
73
- Font actualFont = new Font (consoleFont .getName (), consoleFont .getStyle (), editorFont .getSize ());
75
+ Font actualFont = new Font (consoleFont .getName (), consoleFont .getStyle (), scale ( editorFont .getSize () ));
74
76
75
77
SimpleAttributeSet stdOutStyle = new SimpleAttributeSet ();
76
78
StyleConstants .setForeground (stdOutStyle , Theme .getColor ("console.output.color" ));
Original file line number Diff line number Diff line change @@ -133,6 +133,14 @@ static public Dimension scale(Dimension dim) {
133
133
return new Dimension (scale (dim .width ), scale (dim .height ));
134
134
}
135
135
136
+ static public Font scale (Font font ) {
137
+ float size = scale (font .getSize ());
138
+ // size must be float to call the correct Font.deriveFont(float)
139
+ // method that is different from Font.deriveFont(int)!
140
+ Font scaled = font .deriveFont (size );
141
+ return scaled ;
142
+ }
143
+
136
144
static public Rectangle scale (Rectangle rect ) {
137
145
Rectangle res = new Rectangle (rect );
138
146
res .x = scale (res .x );
You can’t perform that action at this time.
0 commit comments