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 11:48:25 +00:00
parent 6df004a3ed
commit f8ba5d3a69
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,
KeyListener, FocusListener {
private int[] sizes = {14,16,20,25,30,36};
private int[] sizes = {16,18,20,25,30,36};
private String[] envfonts;
private Font font;
Font[] fontObjs;
private static int DEFAULT_FONT_SIZE = 14;
private static int DEFAULT_FONT_SIZE = 16;
private JComboBox fontList;
private JLabel fontLabel = new JLabel(" Font: ");
private JComboBox sizeList;
@@ -280,7 +280,7 @@ public class GFEditor2 extends JFrame implements ActionListener, CaretListener,
output.setSelectionColor(Color.green);
// output.setSelectionColor(Color.white);
// 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);
field.setFont(font);
field.setFocusable(true);
@@ -1024,7 +1024,7 @@ public class GFEditor2 extends JFrame implements ActionListener, CaretListener,
Object obj = ae.getSource();
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);
fontEveryWhere(font);
cbMenuItem.setFont(font);
@@ -1033,7 +1033,7 @@ public class GFEditor2 extends JFrame implements ActionListener, CaretListener,
}
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);
cbMenuItem.setFont(font);
rbMenuItem.setFont(font);