diff options
| author | janna <unknown> | 2004-08-13 12:16:00 +0000 |
|---|---|---|
| committer | janna <unknown> | 2004-08-13 12:16:00 +0000 |
| commit | a7605447420a6acdde087a6bd7be6ef2d0dd12cd (patch) | |
| tree | ed0cf9bc16bef0524476f6d24b4e47ae563537af | |
| parent | f8ba5d3a6900f50f170777b6c0c8b0c1cf61f0be (diff) | |
*** empty log message ***
| -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 ) {
|