From a454e7f6c47387456c53d7eea5096680387dfd03 Mon Sep 17 00:00:00 2001
From: janna <unknown>
Date: Sat, 14 Aug 2004 10:37:29 +0000
Subject: [PATCH] *** empty log message ***

---
 src/JavaGUI/GFEditor2.java | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/JavaGUI/GFEditor2.java b/src/JavaGUI/GFEditor2.java
index 8ca0c3fc1..cf0471134 100644
--- a/src/JavaGUI/GFEditor2.java
+++ b/src/JavaGUI/GFEditor2.java
@@ -18,7 +18,7 @@ public class GFEditor2 extends JFrame implements ActionListener, CaretListener,
     private String[] envfonts;
     private Font font;  
     Font[] fontObjs;
-    private static int DEFAULT_FONT_SIZE = 16;
+    private static int DEFAULT_FONT_SIZE = 14;
     private JComboBox fontList;
     private JLabel fontLabel = new JLabel("   Font: ");
     private JComboBox sizeList;
@@ -371,14 +371,14 @@ public class GFEditor2 extends JFrame implements ActionListener, CaretListener,
         treePanel.setDividerSize(5);
         treePanel.setDividerLocation(100);
         centerPanel2.setLayout(new BorderLayout());
-        gui2.setSize(350,150);
+        gui2.setSize(350,100);
         gui2.setTitle("Select Action on Subterm");
         gui2.setLocationRelativeTo(treePanel);
         centerPanelDown.setLayout(new BorderLayout());
         centerPanel = new JSplitPane(JSplitPane.VERTICAL_SPLIT,
                                    treePanel, centerPanelDown);
         centerPanel.setDividerSize(5);
-        centerPanel.setDividerLocation(350);
+        centerPanel.setDividerLocation(250);
         centerPanel.addKeyListener(tree);      
         centerPanel.setOneTouchExpandable(true);
         centerPanelDown.add(middlePanel, BorderLayout.NORTH);
@@ -447,8 +447,8 @@ public class GFEditor2 extends JFrame implements ActionListener, CaretListener,
         undo.setFocusable(false);  
 
         output.addKeyListener(tree);            
-	setSize(1040,800);
-	outputPanelUp.setPreferredSize(new Dimension(500,300));
+	setSize(800,600);
+	outputPanelUp.setPreferredSize(new Dimension(400,230));
         treePanel.setDividerLocation(0.3);
         nodeTable.put(new TreePath(DynamicTree2.rootNode.getPath()), new Integer(0));
         setVisible(true);