public class JavaReduxFileCollection extends java.lang.Object implements FileCollection
FileCollection
which allows to retrieve the
internally stored java boot sources and to iterate over them.
The resources are stored in the binaries. We use the
KeYResourceManager
to find the resources.
There is a text file whose name is given by
Profile.getInternalClasslistFilename()
which enumerates all java files that have to be read.
Modifier and Type | Class and Description |
---|---|
private class |
JavaReduxFileCollection.Walker |
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
JAVA_SRC_DIR
The location where the libraries to be parsed can be found.
|
private java.lang.String |
resourceLocation
The resource location
|
private java.util.List<java.lang.String> |
resources
This list stores all resources to be retrieved.
|
Constructor and Description |
---|
JavaReduxFileCollection(Profile profile)
Instantiates a new file collection.
|
Modifier and Type | Method and Description |
---|---|
JavaReduxFileCollection.Walker |
createWalker(java.lang.String extension)
create a
FileCollection.Walker object that allows to iterate the file
collection. |
JavaReduxFileCollection.Walker |
createWalker(java.lang.String[] extensions)
create a
FileCollection.Walker object that allows to iterate the file
collection. |
public static final java.lang.String JAVA_SRC_DIR
private java.lang.String resourceLocation
private java.util.List<java.lang.String> resources
public JavaReduxFileCollection(Profile profile) throws java.io.IOException
java.io.IOException
- if access to the resources failspublic JavaReduxFileCollection.Walker createWalker(java.lang.String extension) throws java.io.IOException
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.
This class only supports walker for a single file type: .javacreateWalker
in interface FileCollection
extension
- file extension to be considered only. null if all files
are to be considered.java.io.IOException
- during opening resourcespublic JavaReduxFileCollection.Walker createWalker(java.lang.String[] extensions) throws java.io.IOException
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.
This class only supports walker for a single file type: .javacreateWalker
in interface FileCollection
extensions
- file extensions to be considered only. null if all files
are to be considered.java.io.IOException
- during opening resources