From 4bc5b35bcb4a834c7d22f6503bf5d64e7092cd2b Mon Sep 17 00:00:00 2001
From: janna <unknown>
Date: Wed, 11 Aug 2004 20:21:24 +0000
Subject: [PATCH] *** empty log message ***

---
 src/JavaGUI/GFEditor2.java     | 75 +++++++++++++++++-----------------
 src/JavaGUI/GrammarFilter.java |  4 +-
 src/JavaGUI/Utils.java         |  2 +-
 3 files changed, 41 insertions(+), 40 deletions(-)

diff --git a/src/JavaGUI/GFEditor2.java b/src/JavaGUI/GFEditor2.java
index 9c204bfa3..6b1eb9e2f 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 = 18;
+    private static int DEFAULT_FONT_SIZE = 20;
     private JComboBox fontList;
     private JLabel fontLabel = new JLabel("   Font: ");
     private JComboBox sizeList;
@@ -346,12 +346,8 @@ public class GFEditor2 extends JFrame implements ActionListener, CaretListener,
         }
         sizeList.addActionListener(this);
 
-        sizeList.setFont(font);
-        fontList.setFont(font);
-        menu.setFont(font);
-        filter.setFont(font);
-        modify.setFont(font);
-
+        fontEveryWhere(font);
+      
         upPanel.add(sizeLabel);
         upPanel.add(sizeList);
         upPanel.add(fontLabel);
@@ -733,7 +729,7 @@ System.out.println("encoding "+defaultEncoding);
   
       more = true;
       while (more){
-        if ((result.indexOf("/gf")==-1)&&(result.indexOf("lin")==-1)) {         
+        if ((result.indexOf("/gfinit")==-1)&&(result.indexOf("lin")==-1)) {         
           //form lang and Menu menu: 
           cbMenuItem = new JCheckBoxMenuItem(result.substring(4));
           if (debug) System.out.println ("menu item: "+result.substring(4));   
@@ -772,12 +768,12 @@ System.out.println("encoding "+defaultEncoding);
         // read </language>
         result = fromProc.readLine();
         if (debug) System.out.println("2 "+result); 
-        // read <language> or </gf...>
+        // read <language> or </gfinit...>
         result = fromProc.readLine();
         if (debug) System.out.println("3 "+result); 
-        if ((result.indexOf("/gf")!=-1)||(result.indexOf("lin")!=-1)) 
+        if ((result.indexOf("/gfinit")!=-1)||(result.indexOf("lin")!=-1)) 
           more = false; 
-        if (result.indexOf("/gf")!=-1)
+        if (result.indexOf("/gfinit")!=-1)
           finished = true;
         // registering the file name:
         if (result.indexOf("language")!=-1) {
@@ -950,32 +946,8 @@ System.out.println("encoding "+defaultEncoding);
     }
   }
 
-  public void recursion(JMenu subMenu, Font font)
-  {  
-    for (int i = 0; i<subMenu.getItemCount(); i++)
-      { 
-        JMenuItem item = subMenu.getItem(i);
-        if (item != null) 
-        {
-          item.setFont(font);
-          String name = item.getClass().getName();
-          System.out.println(name);
-        }
-      }
-  }
-
-  public void actionPerformed(ActionEvent ae)
-  {  
-    boolean abs = true;
-    Object obj = ae.getSource();
-
-    if ( obj == fontList ) {
-        font = new Font((String)fontList.getSelectedItem(), Font.PLAIN, ((Integer)sizeList.getSelectedItem()).intValue());
-        output.setFont(font);  
-    }
-
-    if ( obj == sizeList ) {
-        font = new Font((String)fontList.getSelectedItem(), Font.PLAIN, ((Integer)sizeList.getSelectedItem()).intValue());
+  public void fontEveryWhere(Font font)
+  {                          
         output.setFont(font);  
         field.setFont(font);  
         tree.tree.setFont(font);  
@@ -1022,6 +994,35 @@ System.out.println("encoding "+defaultEncoding);
         viewMenu.setFont(font);  
         recursion(viewMenu, font);
 
+}
+
+  public void recursion(JMenu subMenu, Font font)
+  {  
+    for (int i = 0; i<subMenu.getItemCount(); i++)
+      { 
+        JMenuItem item = subMenu.getItem(i);
+        if (item != null) 
+        {
+          item.setFont(font);
+          String name = item.getClass().getName();
+          System.out.println(name);
+        }
+      }
+  }
+
+  public void actionPerformed(ActionEvent ae)
+  {  
+    boolean abs = true;
+    Object obj = ae.getSource();
+
+    if ( obj == fontList ) {
+        font = new Font((String)fontList.getSelectedItem(), Font.PLAIN, ((Integer)sizeList.getSelectedItem()).intValue());
+        output.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);  
diff --git a/src/JavaGUI/GrammarFilter.java b/src/JavaGUI/GrammarFilter.java
index 514da3fa8..5180a9f6e 100644
--- a/src/JavaGUI/GrammarFilter.java
+++ b/src/JavaGUI/GrammarFilter.java
@@ -4,7 +4,7 @@ import javax.swing.filechooser.*;
 
 public class GrammarFilter extends FileFilter {
     
-    // Accept all directories and all gf, gfm files.
+    // Accept all directories and all gf, gfcm files.
     public boolean accept(File f) {
         if (f.isDirectory()) {
             return true;
@@ -13,7 +13,7 @@ public class GrammarFilter extends FileFilter {
         String extension = Utils.getExtension(f);
 	if (extension != null) {
             if (extension.equals(Utils.gf) ||
-                extension.equals(Utils.gfm)) {
+                extension.equals(Utils.gfcm)) {
                     return true;
             } else {
                 return false;
diff --git a/src/JavaGUI/Utils.java b/src/JavaGUI/Utils.java
index f7c6f5b93..b10f54712 100644
--- a/src/JavaGUI/Utils.java
+++ b/src/JavaGUI/Utils.java
@@ -4,7 +4,7 @@ import java.io.File;
 public class Utils {
 
     public final static String gf = "gf";
-    public final static String gfm = "gfm";
+    public final static String gfcm = "gfcm";
 
     /*
      * Get the extension of a file.