public class ZipFileCollection extends java.lang.Object implements FileCollection
Constructor and Description |
---|
ZipFileCollection(java.io.File file) |
Modifier and Type | Method and Description |
---|---|
de.uka.ilkd.key.util.ZipFileCollection.Walker |
createWalker(java.lang.String extension)
create a
FileCollection.Walker object that allows to iterate the file
collection. |
de.uka.ilkd.key.util.ZipFileCollection.Walker |
createWalker(java.lang.String[] extensions)
create a
FileCollection.Walker object that allows to iterate the file
collection. |
java.lang.String |
toString() |
public de.uka.ilkd.key.util.ZipFileCollection.Walker createWalker(java.lang.String[] extensions) throws java.io.IOException
FileCollection
FileCollection.Walker
object that allows to iterate the file
collection.
The search can be restricted to files with a certain extension. If this
is not desired, one specifies null for the extension.createWalker
in interface FileCollection
extensions
- file extensions to be considered only. null if all files
are to be considered.java.io.IOException
- during opening resourcespublic de.uka.ilkd.key.util.ZipFileCollection.Walker createWalker(java.lang.String extension) throws java.io.IOException
FileCollection
FileCollection.Walker
object that allows to iterate the file
collection.
The search can be restricted to files with a certain extension. If this
is not desired, one specifies null for the extension.createWalker
in interface FileCollection
extension
- file extension to be considered only. null if all files
are to be considered.java.io.IOException
- during opening resourcespublic java.lang.String toString()
toString
in class java.lang.Object
Copyright © 2003-2019 The KeY-Project.