diff --git a/src/JavaGUI/GFEditor2.java b/src/JavaGUI/GFEditor2.java index 6b1eb9e2f..b184b8e77 100644 --- a/src/JavaGUI/GFEditor2.java +++ b/src/JavaGUI/GFEditor2.java @@ -14,11 +14,11 @@ import java.util.*; public class GFEditor2 extends JFrame implements ActionListener, CaretListener, KeyListener, FocusListener { - private int[] sizes = {10,12,16,20,25,30,36}; + private int[] sizes = {14,16,20,25,30,36}; private String[] envfonts; private Font font; Font[] fontObjs; - private static int DEFAULT_FONT_SIZE = 20; + private static int DEFAULT_FONT_SIZE = 14; private JComboBox fontList; private JLabel fontLabel = new JLabel(" Font: "); private JComboBox sizeList; @@ -31,7 +31,7 @@ public class GFEditor2 extends JFrame implements ActionListener, CaretListener, public MouseEvent m2; public static String selectedText=""; - public static boolean debug = true; + public static boolean debug = false; public static boolean debug3 = false; public static boolean debug2 = false; public static boolean selectionCheck = false; @@ -101,8 +101,9 @@ public class GFEditor2 extends JFrame implements ActionListener, CaretListener, private JButton alpha = new JButton("Alpha"); private JButton random = new JButton("Random"); private JButton undo = new JButton("Undo"); - + private JPanel coverPanel = new JPanel(); private JPanel inputPanel = new JPanel(); + private JPanel inputPanel2 = new JPanel(); private JPanel inputPanel3 = new JPanel(); private JButton ok = new JButton("OK"); @@ -268,7 +269,9 @@ public class GFEditor2 extends JFrame implements ActionListener, CaretListener, modeMenu.add(rbMenuItemUnTyped); cp = getContentPane(); - cp.setLayout(new BorderLayout()); + JScrollPane cpPanelScroll = new JScrollPane(coverPanel); + cp.add(cpPanelScroll); + coverPanel.setLayout(new BorderLayout()); output.setToolTipText("Linearizations' display area"); output.addCaretListener(this); output.setEditable(false); @@ -277,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.PLAIN, 20); + font = new Font(null, Font.BOLD, DEFAULT_FONT_SIZE); output.setFont(font); field.setFont(font); field.setFocusable(true); @@ -339,7 +342,10 @@ public class GFEditor2 extends JFrame implements ActionListener, CaretListener, } fontList = new JComboBox(envfonts); fontList.addActionListener(this); + fontList.setToolTipText("Changing font type"); + sizeList = new JComboBox(); + sizeList.setToolTipText("Changing font size"); for (int i = 0; i