Class DefaultFileFilter.EditorFileFilter
- java.lang.Object
-
- javax.swing.filechooser.FileFilter
-
- org.processmining.objectcentricconstraintchecking.algorithms.editor.DefaultFileFilter.EditorFileFilter
-
- Enclosing class:
- DefaultFileFilter
public static class DefaultFileFilter.EditorFileFilter extends javax.swing.filechooser.FileFilterUtility file filter to accept editor files, namely .xml and .xml.gz extensions.- See Also:
ImageIO.getReaderFormatNames()
-
-
Field Summary
Fields Modifier and Type Field Description protected java.lang.StringdescDescription of the File format
-
Constructor Summary
Constructors Constructor Description EditorFileFilter(java.lang.String description)Constructs a new editor file filter using the specified description.
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description booleanaccept(java.io.File file)Returns true if the file is a directory or has a .xml or .xml.gz extension.java.lang.StringgetDescription()Returns the description.
-
-
-
Method Detail
-
accept
public boolean accept(java.io.File file)
Returns true if the file is a directory or has a .xml or .xml.gz extension.- Specified by:
acceptin classjavax.swing.filechooser.FileFilter- Returns:
- Returns true if the file is accepted.
-
getDescription
public java.lang.String getDescription()
Returns the description.- Specified by:
getDescriptionin classjavax.swing.filechooser.FileFilter- Returns:
- Returns the description.
-
-