Class DITFileFilter

java.lang.Object
  |
  +--javax.swing.filechooser.FileFilter
        |
        +--DITFileFilter

public class DITFileFilter

extends javax.swing.filechooser.FileFilter

File filter - show only data files of the Isabelle Tool : *.dit = any file with extention D(ata for) I(sabelle's) T(ool) The file extention is kept though the software has got a more grownup name : Echo *.tpl is the other extention used by Echo - for templates A convenience implementation of FileFilter that filters out all files except for those type extensions that it knows about. Extensions are of the type ".foo", which is typically found on Windows and Unix boxes, but not on Macinthosh. Case is ignored. To use without DITFileChoser : create a new filter that filerts out all files but gif and jpg image files: JFileChooser chooser = new JFileChooser(); DITFileFilter filter = new DITFileFilter( new String{"gif", "jpg"}, "JPEG & GIF Images") chooser.addChoosableFileFilter(filter); chooser.showOpenDialog(this); but all this is done in DITFileChoser

Constructor Summary

DITFileFilter()
Creates a file filter.

DITFileFilter(java.lang.String extension)
Creates a file filter that accepts files with the given extension.

DITFileFilter(java.lang.String[] filters)
Creates a file filter from the given string array.

DITFileFilter(java.lang.String[] filters, java.lang.String description)
Creates a file filter from the given string array and description.

DITFileFilter(java.lang.String extension, java.lang.String description)
Creates a file filter that accepts the given file type.

Method Summary

boolean	accept(java.io.File f) Return true if this file should be shown in the directory pane, false if it shouldn't.
void	addExtension(java.lang.String extension) Adds a filetype "dot" extension to filter against.
java.lang.String	getDescription() Returns the human readable description of this filter.
java.lang.String	getExtension(java.io.File f) Return the extension portion of the file's name .
boolean	isExtensionListInDescription() Returns whether the extension list (.jpg, .gif, etc) should show up in the human readable description.
void	setDescription(java.lang.String description) Sets the human readable description of this filter.
void	setExtensionListInDescription(boolean b) Determines whether the extension list (.jpg, .gif, etc) should show up in the human readable description.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

DITFileFilter

public DITFileFilter()

Creates a file filter. If no filters are added, then all files are accepted.

DITFileFilter

public DITFileFilter(java.lang.String extension)

Creates a file filter that accepts files with the given extension. Example: new DITFileFilter("jpg");

DITFileFilter

public DITFileFilter(java.lang.String extension,
                     java.lang.String description)

Creates a file filter that accepts the given file type. Example: new DITFileFilter("jpg", "JPEG Image Images"); Note that the "." before the extension is not needed. If provided, it will be ignored.

DITFileFilter

public DITFileFilter(java.lang.String[] filters)

Creates a file filter from the given string array. Example: new DITFileFilter(String {"gif", "jpg"}); Note that the "." before the extension is not needed adn will be ignored.

DITFileFilter

public DITFileFilter(java.lang.String[] filters,
                     java.lang.String description)

Creates a file filter from the given string array and description. Example: new DITFileFilter(String {"gif", "jpg"}, "Gif and JPG Images"); Note that the "." before the extension is not needed and will be ignored.

Method Detail

accept

public boolean accept(java.io.File f)

Return true if this file should be shown in the directory pane, false if it shouldn't. Files that begin with "." are ignored.

Overrides:

accept in class javax.swing.filechooser.FileFilter

getExtension

public java.lang.String getExtension(java.io.File f)

Return the extension portion of the file's name .

addExtension

public void addExtension(java.lang.String extension)

Adds a filetype "dot" extension to filter against. For example: the following code will create a filter that filters out all files except those that end in ".jpg" and ".tif": DITFileFilter filter = new DITFileFilter(); filter.addExtension("jpg"); filter.addExtension("tif"); Note that the "." before the extension is not needed and will be ignored.

getDescription

public java.lang.String getDescription()

Returns the human readable description of this filter. For example: "JPEG and GIF Image Files (*.jpg, *.gif)"

Overrides:

getDescription in class javax.swing.filechooser.FileFilter

setDescription

public void setDescription(java.lang.String description)

Sets the human readable description of this filter. For example: filter.setDescription("Gif and JPG Images");

setExtensionListInDescription

public void setExtensionListInDescription(boolean b)

Determines whether the extension list (.jpg, .gif, etc) should show up in the human readable description. Only relevent if a description was provided in the constructor or using setDescription();

isExtensionListInDescription

public boolean isExtensionListInDescription()

Returns whether the extension list (.jpg, .gif, etc) should show up in the human readable description. Only relevent if a description was provided in the constructor or using setDescription();