diff options
| -rw-r--r-- | src/JavaGUI/GFEditor2.java | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/JavaGUI/GFEditor2.java b/src/JavaGUI/GFEditor2.java index 12a265741..8ca0c3fc1 100644 --- a/src/JavaGUI/GFEditor2.java +++ b/src/JavaGUI/GFEditor2.java @@ -14,7 +14,7 @@ import java.util.*; public class GFEditor2 extends JFrame implements ActionListener, CaretListener,
KeyListener, FocusListener {
- private int[] sizes = {16,18,20,25,30,36};
+ private int[] sizes = {14,18,22,26,30};
private String[] envfonts;
private Font font;
Font[] fontObjs;
@@ -1027,17 +1027,17 @@ public class GFEditor2 extends JFrame implements ActionListener, CaretListener, font = new Font((String)fontList.getSelectedItem(), Font.PLAIN, ((Integer)sizeList.getSelectedItem()).intValue());
//output.setFont(font);
fontEveryWhere(font);
- cbMenuItem.setFont(font);
- rbMenuItem.setFont(font);
- fileMenuItem.setFont(font);
+ if (cbMenuItem!=null) cbMenuItem.setFont(font);
+ if (rbMenuItem!=null) rbMenuItem.setFont(font);
+ if (fileMenuItem!=null) fileMenuItem.setFont(font);
}
if ( obj == sizeList ) {
font = new Font((String)fontList.getSelectedItem(), Font.PLAIN, ((Integer)sizeList.getSelectedItem()).intValue());
fontEveryWhere(font);
- cbMenuItem.setFont(font);
- rbMenuItem.setFont(font);
- fileMenuItem.setFont(font);
+ if (cbMenuItem!=null) cbMenuItem.setFont(font);
+ if (rbMenuItem!=null) rbMenuItem.setFont(font);
+ if (fileMenuItem!=null) fileMenuItem.setFont(font);
}
if ( obj == menu ) {
|