de.uka.ilkd.key.util

Interface FileCollection.Walker

All Known Implementing Classes:

DirectoryFileCollection.Walker, JavaReduxFileCollection.Walker, ZipFileCollection.Walker

Enclosing interface:

FileCollection

public static interface FileCollection.Walker

A Walker allows to iterate (once and one way) through a FileCollection.

Method Summary

Modifier and Type	Method and Description
DataLocation	getCurrentDataLocation() get a DataLocation object describing the current file.
java.lang.String	getCurrentName() get the name of the current file in the iteration.
java.lang.String	getType() return the type of the structure that is iterated.
java.io.InputStream	openCurrent() create a new InputStream for the current element of the iteration.
boolean	step() step to next element in the collection if there is another one.

Method Detail

step

boolean step()

step to next element in the collection if there is another one. The getCurrent...() functions will behave differently after a call to step().

Returns:

true iff there is another element in the collection

getCurrentName

java.lang.String getCurrentName()
                         throws java.util.NoSuchElementException

get the name of the current file in the iteration. This is only the short name not including any location data.

Returns:

a short file name, not null

Throws:

java.util.NoSuchElementException - if the previous call to step returned false.

getCurrentDataLocation

DataLocation getCurrentDataLocation()
                             throws java.util.NoSuchElementException

get a DataLocation object describing the current file. The dynamic type of the result depends on the implementation in use.

Returns:

a DataLocation, not null

Throws:

java.util.NoSuchElementException - if the previous call to step returned false.

getType

java.lang.String getType()

return the type of the structure that is iterated. Must return the same value for any call

Returns:

a non-null String describing the type (e.g. "zip" or "file");

Throws:

java.util.NoSuchElementException - if the previous call to step returned false.

openCurrent

java.io.InputStream openCurrent()
                         throws java.io.IOException,
                                java.util.NoSuchElementException

create a new InputStream for the current element of the iteration. It is in the user's obligation to close the stream after using it.

Returns:

a freshly created InputStream, the dynamic type depends on the implementation

Throws:

java.io.IOException - if the resource cannot be opened

java.util.NoSuchElementException - if the previous call to step returned false.