JmlGUI.AllFilesGUIFileFilter (JML and MultiJava documentation)

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

JML

PREV CLASS NEXT CLASS

FRAMES NO FRAMES

SUMMARY: NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

org.jmlspecs.checker
Class JmlGUI.AllFilesGUIFileFilter

java.lang.Object
  javax.swing.filechooser.FileFilter
      org.multijava.util.gui.GUI.GUIFileFilter
          org.jmlspecs.checker.JmlGUI.AllFilesGUIFileFilter

Enclosing class:: JmlGUI

protected class JmlGUI.AllFilesGUIFileFilter
extends org.multijava.util.gui.GUI.GUIFileFilter

Constructor Summary

protected JmlGUI.AllFilesGUIFileFilter()


Method Summary

String getDescription()


boolean hasActiveSuffix(String name)


Methods inherited from class org.multijava.util.gui.GUI.GUIFileFilter

accept

Methods inherited from class java.lang.Object

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

Constructor Detail

JmlGUI.AllFilesGUIFileFilter

protected JmlGUI.AllFilesGUIFileFilter()

Method Detail

hasActiveSuffix

public boolean hasActiveSuffix(String name)

getDescription

public String getDescription()