public final class RavenFileFilter extends FileFilter
FileFilter
that filters the set of files shown
to the user based on the file name extension. The filter accepts only those
files which are relevant for Raven.FileFilter
,
JFileChooser
,
RavenMain
Modifier and Type | Field and Description |
---|---|
static FileFilter |
DEFAULT_AUTOMATON_FILE_FILTER
Automaton File Filter
|
static FileFilter |
DEFAULT_COSPAN_FILE_FILTER
Cospan File Filter
|
static FileFilter |
DEFAULT_DECOMPOSITION_FILE_FILTER
Decomposition File Filter
|
static FileFilter |
DEFAULT_SIGNATURE_FILE_FILTER
Signature File Filter
|
static FileFilter |
GRAPH_GXL_FILE_FILTER
Graph GXL File Filter
|
static FileFilter |
GRAPH_SVG_FILE_FILTER
Graph SVG File Filter
|
static FileFilter |
RAVEN_SCRIPT_FILE_FILTER
Raven Script File Filter
|
public static final FileFilter DEFAULT_AUTOMATON_FILE_FILTER
public static final FileFilter DEFAULT_COSPAN_FILE_FILTER
public static final FileFilter DEFAULT_DECOMPOSITION_FILE_FILTER
public static final FileFilter GRAPH_GXL_FILE_FILTER
public static final FileFilter GRAPH_SVG_FILE_FILTER
public static final FileFilter DEFAULT_SIGNATURE_FILE_FILTER
public static final FileFilter RAVEN_SCRIPT_FILE_FILTER
public boolean accept(File f)
accept
in class FileFilter
public String getDescription()
getDescription
in class FileFilter