diff options
| author | aarne <unknown> | 2005-06-30 22:09:36 +0000 |
|---|---|---|
| committer | aarne <unknown> | 2005-06-30 22:09:36 +0000 |
| commit | 4d94cdfd66c63eb01ad90c292f3dc75878a0e8a7 (patch) | |
| tree | 59eb283aeb626419b5f5b0beae48827e2eb0ba48 /src/JavaGUI2/de/uka/ilkd/key/ocl | |
| parent | 7bb9e88cb875372bd3e288b8831b1b60c3b9bc17 (diff) | |
gfcm in Java ; Finnish close to finished
Diffstat (limited to 'src/JavaGUI2/de/uka/ilkd/key/ocl')
| -rw-r--r-- | src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GrammarFilter.java | 6 | ||||
| -rw-r--r-- | src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Utils.java | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GrammarFilter.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GrammarFilter.java index 13d8f5184..e8bd59c66 100644 --- a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GrammarFilter.java +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GrammarFilter.java @@ -20,7 +20,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; @@ -29,7 +29,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; @@ -41,6 +41,6 @@ public class GrammarFilter extends FileFilter { // The description of this filter public String getDescription() { - return "Just Grammars (*.gf, *.gfm)"; + return "Just Grammars (*.gf, *.gfcm)"; } } diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Utils.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Utils.java index e8b67e72b..fc93852a2 100644 --- a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Utils.java +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Utils.java @@ -30,7 +30,7 @@ public class Utils { } public static final String gf = "gf"; - public static final String gfm = "gfm"; + public static final String gfcm = "gfcm"; /* * Get the extension of a file. |