JmldocGUI.JmldocGUIFileFilter (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.jmldoc.jmldoc_142
Class JmldocGUI.JmldocGUIFileFilter

java.lang.Object
  javax.swing.filechooser.FileFilter
      org.multijava.util.gui.GUI.GUIFileFilter
          org.jmlspecs.jmldoc.jmldoc_142.JmldocGUI.JmldocGUIFileFilter

Enclosing class:: JmldocGUI

protected class JmldocGUI.JmldocGUIFileFilter
extends org.multijava.util.gui.GUI.GUIFileFilter

Field Summary

(package private) String suffix


Constructor Summary

JmldocGUI.JmldocGUIFileFilter(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

JmldocGUI.JmldocGUIFileFilter

public JmldocGUI.JmldocGUIFileFilter(String suffix)

Method Detail

hasActiveSuffix

public boolean hasActiveSuffix(String name)

getDescription

public String getDescription()