public interface EnvInput
Modifier and Type | Method and Description |
---|---|
java.io.File |
getInitialFile()
Returns the initial
File which is loaded if available. |
int |
getNumberOfChars()
Returns the total numbers of chars that can be read in this input.
|
Profile |
getProfile()
Returns the
Profile to use. |
java.lang.String |
name()
Returns the name of this input.
|
ImmutableSet<PositionedString> |
read()
Reads the input using the given modification strategy, i.e.,
parts of the input do not modify the initial configuration while
others do.
|
java.io.File |
readBootClassPath()
gets the boot classpath element, null if none set.
|
java.util.List<java.io.File> |
readClassPath()
gets the classpath elements to be considered here.
|
Includes |
readIncludes()
Reads the include section and returns an Includes object.
|
java.lang.String |
readJavaPath()
Reads the Java path.
|
void |
setInitConfig(InitConfig initConfig)
Sets the initial configuration the read environment input should be
added to.
|
java.lang.String name()
int getNumberOfChars()
void setInitConfig(InitConfig initConfig)
Includes readIncludes() throws ProofInputException
ProofInputException
java.lang.String readJavaPath() throws ProofInputException
ProofInputException
java.util.List<java.io.File> readClassPath() throws ProofInputException
ProofInputException
java.io.File readBootClassPath() throws java.io.IOException
java.io.IOException
ImmutableSet<PositionedString> read() throws ProofInputException
ImmutableSet
if no warnings occurred.ProofInputException
java.io.File getInitialFile()
File
which is loaded if available.File
which is loaded or null
otherwise.