GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-04-09 04:59:31 -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 5cd8b33302
commit ad3fd6c082
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,
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 ) {