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

*** empty log message ***

Browse Source
This commit is contained in:
janna
2004-08-11 20:21:24 +00:00
parent 29e2201eef
commit 1b3f318ae8
3 changed files with 41 additions and 40 deletions
Download Patch File Download Diff File Expand all files Collapse all files

75
src/JavaGUI/GFEditor2.java
View File

@@ -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);

4
src/JavaGUI/GrammarFilter.java
View File

@@ -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;

2
src/JavaGUI/Utils.java
View File

@@ -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.