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

*** empty log message ***

Browse Source
This commit is contained in:
janna
2004-08-13 11:48:25 +00:00
parent 5eb8d24629
commit 5cd8b33302
1 changed files with 5 additions and 5 deletions
Download Patch File Download Diff File Expand all files Collapse all files

10
src/JavaGUI/GFEditor2.java
View File

@@ -14,11 +14,11 @@ 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 = {14,16,20,25,30,36}; private int[] sizes = {16,18,20,25,30,36};
private String[] envfonts; private String[] envfonts;
private Font font; private Font font;
Font[] fontObjs; Font[] fontObjs;
private static int DEFAULT_FONT_SIZE = 14; private static int DEFAULT_FONT_SIZE = 16;
private JComboBox fontList; private JComboBox fontList;
private JLabel fontLabel = new JLabel(" Font: "); private JLabel fontLabel = new JLabel(" Font: ");
private JComboBox sizeList; private JComboBox sizeList;
@@ -280,7 +280,7 @@ public class GFEditor2 extends JFrame implements ActionListener, CaretListener,
output.setSelectionColor(Color.green); output.setSelectionColor(Color.green);
// output.setSelectionColor(Color.white); // output.setSelectionColor(Color.white);
// output.setFont(new Font("Arial Unicode MS", Font.PLAIN, 17)); // output.setFont(new Font("Arial Unicode MS", Font.PLAIN, 17));
font = new Font(null, Font.BOLD, DEFAULT_FONT_SIZE); font = new Font(null, Font.PLAIN, DEFAULT_FONT_SIZE);
output.setFont(font); output.setFont(font);
field.setFont(font); field.setFont(font);
field.setFocusable(true); field.setFocusable(true);
@@ -1024,7 +1024,7 @@ public class GFEditor2 extends JFrame implements ActionListener, CaretListener,
Object obj = ae.getSource(); Object obj = ae.getSource();
if ( obj == fontList ) { if ( obj == fontList ) {
font = new Font((String)fontList.getSelectedItem(), Font.BOLD, ((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); cbMenuItem.setFont(font);
@@ -1033,7 +1033,7 @@ public class GFEditor2 extends JFrame implements ActionListener, CaretListener,
} }
if ( obj == sizeList ) { if ( obj == sizeList ) {
font = new Font((String)fontList.getSelectedItem(), Font.BOLD, ((Integer)sizeList.getSelectedItem()).intValue()); font = new Font((String)fontList.getSelectedItem(), Font.PLAIN, ((Integer)sizeList.getSelectedItem()).intValue());
fontEveryWhere(font); fontEveryWhere(font);
cbMenuItem.setFont(font); cbMenuItem.setFont(font);
rbMenuItem.setFont(font); rbMenuItem.setFont(font);