GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-04-23 11:42:49 -06:00
Code Issues Packages Projects Releases Wiki Activity

*** empty log message ***

Browse Source
This commit is contained in:
janna
2004-08-13 12:16:00 +00:00
parent f8ba5d3a69
commit a760544742
1 changed files with 7 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

14
src/JavaGUI/GFEditor2.java
View File

@@ -14,7 +14,7 @@ import java.util.*;
public class GFEditor2 extends JFrame implements ActionListener, CaretListener, public class GFEditor2 extends JFrame implements ActionListener, CaretListener,
KeyListener, FocusListener { KeyListener, FocusListener {
private int[] sizes = {16,18,20,25,30,36}; private int[] sizes = {14,18,22,26,30};
private String[] envfonts; private String[] envfonts;
private Font font; private Font font;
Font[] fontObjs; 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()); font = new Font((String)fontList.getSelectedItem(), Font.PLAIN, ((Integer)sizeList.getSelectedItem()).intValue());
//output.setFont(font); //output.setFont(font);
fontEveryWhere(font); fontEveryWhere(font);
cbMenuItem.setFont(font); if (cbMenuItem!=null) cbMenuItem.setFont(font);
rbMenuItem.setFont(font); if (rbMenuItem!=null) rbMenuItem.setFont(font);
fileMenuItem.setFont(font); if (fileMenuItem!=null) fileMenuItem.setFont(font);
} }
if ( obj == sizeList ) { if ( obj == sizeList ) {
font = new Font((String)fontList.getSelectedItem(), Font.PLAIN, ((Integer)sizeList.getSelectedItem()).intValue()); font = new Font((String)fontList.getSelectedItem(), Font.PLAIN, ((Integer)sizeList.getSelectedItem()).intValue());
fontEveryWhere(font); fontEveryWhere(font);
cbMenuItem.setFont(font); if (cbMenuItem!=null) cbMenuItem.setFont(font);
rbMenuItem.setFont(font); if (rbMenuItem!=null) rbMenuItem.setFont(font);
fileMenuItem.setFont(font); if (fileMenuItem!=null) fileMenuItem.setFont(font);
} }
if ( obj == menu ) { if ( obj == menu ) {