extensionfilter.java
来自「Petri网分析工具PIPE is open-source」· Java 代码 · 共 33 行
JAVA
33 行
//######################################################################################/* * Created on 16-Feb-2004 * *///######################################################################################package pipe.gui;//######################################################################################import java.io.File;import javax.swing.filechooser.FileFilter;//######################################################################################public class ExtensionFilter extends FileFilter {//###################################################################################### protected String myExtensionString; // The extension we will accept protected String myExtensionDesc; // A description of its meaning//###################################################################################### public ExtensionFilter(String ext, String desc) { myExtensionString = ext.toLowerCase(); myExtensionDesc = desc; }//###################################################################################### public boolean accept(File f) { return f.isDirectory() || f.getName().toLowerCase().endsWith(myExtensionString); } // Don't want directories, especially ones which end with the desired extension!//###################################################################################### public String getDescription() { return myExtensionDesc; }//######################################################################################}//######################################################################################
⌨️ 快捷键说明
复制代码Ctrl + C
搜索代码Ctrl + F
全屏模式F11
增大字号Ctrl + =
减小字号Ctrl + -
显示快捷键?