1010 */
1111package processing .app .syntax ;
1212
13+ import java .awt .Cursor ;
14+ import java .awt .Dimension ;
15+ import java .awt .Font ;
16+ import java .awt .FontMetrics ;
17+ import java .awt .Graphics ;
18+ import java .awt .Graphics2D ;
19+ import java .awt .Rectangle ;
20+ import java .awt .RenderingHints ;
1321import java .awt .event .MouseEvent ;
14- import java .awt .*;
1522
1623import javax .swing .ToolTipManager ;
1724import javax .swing .text .*;
1825import javax .swing .JComponent ;
1926
2027import processing .app .Preferences ;
2128import processing .app .syntax .im .CompositionTextPainter ;
29+ import processing .app .ui .Toolkit ;
2230
2331
2432/**
@@ -107,12 +115,13 @@ public TextAreaPainter(JEditTextArea textArea, TextAreaDefaults defaults) {
107115
108116
109117 public void updateAppearance () {
110- // // unfortunately probably can't just do setDefaults() since things aren't quite set up
111- // setFont(defaults.plainFont);
112- //// System.out.println("defaults font is " + defaults.font);
113118 setForeground (defaults .fgcolor );
114119 setBackground (defaults .bgcolor );
115120
121+ // Ensure that our monospaced font is loaded
122+ // https://github.com/processing/processing/pull/4639
123+ Toolkit .getMonoFontName ();
124+
116125 String fontFamily = Preferences .get ("editor.font.family" );
117126 int fontSize = Preferences .getInteger ("editor.font.size" );
118127 plainFont = new Font (fontFamily , Font .PLAIN , fontSize );
@@ -124,16 +133,11 @@ public void updateAppearance() {
124133 }
125134 boldFont = new Font (fontFamily , Font .BOLD , fontSize );
126135 antialias = Preferences .getBoolean ("editor.smooth" );
127- // System.out.println(plainFont.getFamily());
128- // System.out.println(plainFont);
129136
130137 // moved from setFont() override (never quite comfortable w/ that override)
131138 fm = super .getFontMetrics (plainFont );
132139 tabSize = fm .charWidth (' ' ) * Preferences .getInteger ("editor.tabs.size" );
133140 textArea .recalculateVisibleLines ();
134-
135- // fgcolor = mode.getColor("editor.fgcolor");
136- // bgcolor = mode.getColor("editor.bgcolor");
137141 }
138142
139143
0 commit comments