JmlGUI.JmlGUIFileFilter (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.JmlGUIFileFilter

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

Enclosing class:: JmlGUI

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

Field Summary

(package private) String suffix


Constructor Summary

JmlGUI.JmlGUIFileFilter(String suffix)


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

Field Detail

suffix

String suffix

Constructor Detail

JmlGUI.JmlGUIFileFilter

public JmlGUI.JmlGUIFileFilter(String suffix)

Method Detail

hasActiveSuffix

public boolean hasActiveSuffix(String name)

getDescription

public String getDescription()