public class KeYEnvironment<U extends UserInterfaceControl>
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private boolean |
disposed
Indicates that this
KeYEnvironment is disposed. |
private InitConfig |
initConfig
The loaded project.
|
private Proof |
loadedProof
An optional
Proof which was loaded by the specified proof file. |
private Pair<java.lang.String,Location> |
proofScript
An optional field denoting a script contained in the proof file.
|
private AbstractProblemLoader.ReplayResult |
replayResult
The
AbstractProblemLoader.ReplayResult if available. |
private U |
ui
The
UserInterfaceControl in which the Proof is loaded. |
Constructor and Description |
---|
KeYEnvironment(U ui,
InitConfig initConfig)
Constructor
|
KeYEnvironment(U ui,
InitConfig initConfig,
Proof loadedProof,
Pair<java.lang.String,Location> proofScript,
AbstractProblemLoader.ReplayResult replayResult)
Constructor
|
Modifier and Type | Method and Description |
---|---|
Proof |
createProof(ProofOblInput input)
Creates a new
Proof with help of the UserInterfaceControl . |
void |
dispose()
Disposes this
KeYEnvironment . |
InitConfig |
getInitConfig()
Returns the loaded project.
|
JavaInfo |
getJavaInfo()
Returns the used
JavaInfo . |
Proof |
getLoadedProof()
Returns the loaded
Proof if a proof file was loaded. |
Profile |
getProfile() |
ProofControl |
getProofControl()
Returns the
ProofControl of getUi() . |
Pair<java.lang.String,Location> |
getProofScript() |
AbstractProblemLoader.ReplayResult |
getReplayResult()
Returns the
AbstractProblemLoader.ReplayResult if available. |
Services |
getServices()
Returns the
Services of getInitConfig() . |
SpecificationRepository |
getSpecificationRepository()
Returns the used
SpecificationRepository . |
U |
getUi()
Returns the
UserInterfaceControl in which the Proof is loaded. |
boolean |
isDisposed()
Checks if this
KeYEnvironment is disposed meaning that
dispose() was already executed at least once. |
static KeYEnvironment<DefaultUserInterfaceControl> |
load(java.io.File keyFile) |
static KeYEnvironment<DefaultUserInterfaceControl> |
load(java.io.File location,
java.util.List<java.io.File> classPaths,
java.io.File bootClassPath,
java.util.List<java.io.File> includes)
Loads the given location and returns all required references as
KeYEnvironment . |
static KeYEnvironment<DefaultUserInterfaceControl> |
load(java.io.File location,
java.util.List<java.io.File> classPaths,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
RuleCompletionHandler ruleCompletionHandler)
Loads the given location and returns all required references as
KeYEnvironment . |
static KeYEnvironment<DefaultUserInterfaceControl> |
load(Profile profile,
java.io.File location,
java.util.List<java.io.File> classPaths,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
boolean forceNewProfileOfNewProofs)
Loads the given location and returns all required references as
KeYEnvironment . |
static KeYEnvironment<DefaultUserInterfaceControl> |
load(Profile profile,
java.io.File location,
java.util.List<java.io.File> classPaths,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
java.util.Properties poPropertiesToForce,
RuleCompletionHandler ruleCompletionHandler,
boolean forceNewProfileOfNewProofs)
Loads the given location and returns all required references as
KeYEnvironment . |
private final U extends UserInterfaceControl ui
UserInterfaceControl
in which the Proof
is loaded.private final InitConfig initConfig
private final Proof loadedProof
Proof
which was loaded by the specified proof file.private final Pair<java.lang.String,Location> proofScript
private boolean disposed
KeYEnvironment
is disposed.private final AbstractProblemLoader.ReplayResult replayResult
AbstractProblemLoader.ReplayResult
if available.public KeYEnvironment(U ui, InitConfig initConfig)
ui
- The UserInterfaceControl
in which the Proof
is loaded.initConfig
- The loaded project.public KeYEnvironment(U ui, InitConfig initConfig, Proof loadedProof, Pair<java.lang.String,Location> proofScript, AbstractProblemLoader.ReplayResult replayResult)
ui
- The UserInterfaceControl
in which the Proof
is loaded.initConfig
- The loaded project.public U getUi()
UserInterfaceControl
in which the Proof
is loaded.UserInterfaceControl
in which the Proof
is loaded.public ProofControl getProofControl()
ProofControl
of getUi()
.ProofControl
of getUi()
.public InitConfig getInitConfig()
public Services getServices()
Services
of getInitConfig()
.Services
of getInitConfig()
.public SpecificationRepository getSpecificationRepository()
SpecificationRepository
.SpecificationRepository
.public Profile getProfile()
public Proof getLoadedProof()
Proof
if a proof file was loaded.Proof
if available and null
otherwise.public AbstractProblemLoader.ReplayResult getReplayResult()
AbstractProblemLoader.ReplayResult
if available.AbstractProblemLoader.ReplayResult
or null
if not available.public Proof createProof(ProofOblInput input) throws ProofInputException
Proof
with help of the UserInterfaceControl
.input
- The ProofOblInput
to instantiate Proof
from.Proof
.ProofInputException
- Occurred Exception.public static KeYEnvironment<DefaultUserInterfaceControl> load(java.io.File location, java.util.List<java.io.File> classPaths, java.io.File bootClassPath, java.util.List<java.io.File> includes) throws ProblemLoaderException
KeYEnvironment
.
The MainWindow
is not involved in the whole process.location
- The location to load.classPaths
- The class path entries to use.bootClassPath
- The boot class path to use.includes
- Optional includes to consider.KeYEnvironment
which contains all references to the loaded location.ProblemLoaderException
- Occurred Exceptionpublic static KeYEnvironment<DefaultUserInterfaceControl> load(java.io.File location, java.util.List<java.io.File> classPaths, java.io.File bootClassPath, java.util.List<java.io.File> includes, RuleCompletionHandler ruleCompletionHandler) throws ProblemLoaderException
KeYEnvironment
.
The MainWindow
is not involved in the whole process.location
- The location to load.classPaths
- The class path entries to use.bootClassPath
- The boot class path to use.includes
- Optional includes to consider.ruleCompletionHandler
- An optional RuleCompletionHandler
.KeYEnvironment
which contains all references to the loaded location.ProblemLoaderException
- Occurred Exceptionpublic static KeYEnvironment<DefaultUserInterfaceControl> load(Profile profile, java.io.File location, java.util.List<java.io.File> classPaths, java.io.File bootClassPath, java.util.List<java.io.File> includes, boolean forceNewProfileOfNewProofs) throws ProblemLoaderException
KeYEnvironment
.
The MainWindow
is not involved in the whole process.profile
- The Profile
to use.location
- The location to load.classPaths
- The class path entries to use.bootClassPath
- The boot class path to use.includes
- Optional includes to consider.forceNewProfileOfNewProofs
- true #profileOfNewProofs
will be used as Profile
of new proofs, false
Profile
specified by problem file will be used for new proofs.KeYEnvironment
which contains all references to the loaded location.ProblemLoaderException
- Occurred Exceptionpublic static KeYEnvironment<DefaultUserInterfaceControl> load(Profile profile, java.io.File location, java.util.List<java.io.File> classPaths, java.io.File bootClassPath, java.util.List<java.io.File> includes, java.util.Properties poPropertiesToForce, RuleCompletionHandler ruleCompletionHandler, boolean forceNewProfileOfNewProofs) throws ProblemLoaderException
KeYEnvironment
.
The MainWindow
is not involved in the whole process.profile
- The Profile
to use.location
- The location to load.classPaths
- The class path entries to use.bootClassPath
- The boot class path to use.includes
- Optional includes to consider.poPropertiesToForce
- Some optional PO Properties
to force.ruleCompletionHandler
- An optional RuleCompletionHandler
.forceNewProfileOfNewProofs
- true
AbstractProblemLoader.profileOfNewProofs
will be used as
Profile
of new proofs, false
Profile
specified by problem file will be used for new proofs.KeYEnvironment
which contains all references to the loaded location.ProblemLoaderException
- Occurred Exceptionpublic static KeYEnvironment<DefaultUserInterfaceControl> load(java.io.File keyFile) throws ProblemLoaderException
ProblemLoaderException
public void dispose()
KeYEnvironment
.public boolean isDisposed()
KeYEnvironment
is disposed meaning that
dispose()
was already executed at least once.true
disposed, false
not disposed and still functionable.