public class JavaReduxFileCollection extends 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 String |
JAVA_SRC_DIR
The location where the libraries to be parsed can be found.
|
private String |
resourceLocation
The resource location
|
private List<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(String extension)
create a
FileCollection.Walker object that allows to iterate the file
collection. |
JavaReduxFileCollection.Walker |
createWalker(String[] extensions)
create a
FileCollection.Walker object that allows to iterate the file
collection. |
public static final String JAVA_SRC_DIR
private String resourceLocation
public JavaReduxFileCollection(Profile profile) throws IOException
IOException
- if access to the resources failspublic JavaReduxFileCollection.Walker createWalker(String extension) throws 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.IOException
- during opening resourcespublic JavaReduxFileCollection.Walker createWalker(String[] extensions) throws 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.IOException
- during opening resources