public abstract class AbstractUserInterfaceControl extends java.lang.Object implements UserInterfaceControl, ProblemLoaderControl, ProverTaskListener
UserInterfaceControl
.Modifier and Type | Class and Description |
---|---|
private class |
AbstractUserInterfaceControl.ProofMacroListenerAdapter |
ProgressMonitor.Empty
Modifier and Type | Field and Description |
---|---|
private int |
numOfInvokedMacros |
private java.util.List<ProverTaskListener> |
proverTaskListener
The registered
ProverTaskListener . |
Constructor and Description |
---|
AbstractUserInterfaceControl()
Constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
addProverTaskListener(ProverTaskListener ptl)
Registers the given
ProverTaskListener which will be informed about all events. |
protected ProblemInitializer |
createProblemInitializer(Profile profile)
Creates a new
ProblemInitializer instance which is configured
for this UserInterfaceControl . |
Proof |
createProof(InitConfig initConfig,
ProofOblInput input)
Instantiates a new
Proof in this UserInterfaceControl for the given
ProofOblInput based on the InitConfig . |
protected abstract ProofEnvironment |
createProofEnvironmentAndRegisterProof(ProofOblInput proofOblInput,
ProofAggregate proofList,
InitConfig initConfig)
registers the proof aggregate at the UI
|
protected void |
fireTaskFinished(TaskFinishedInfo info)
Fires the event
ProverTaskListener.taskFinished(TaskFinishedInfo) to all listener. |
protected void |
fireTaskProgress(int position)
Fires the event
ProverTaskListener.taskProgress(int) to all listener. |
protected void |
fireTaskStarted(TaskStartedInfo info)
Fires the event
ProverTaskListener.taskStarted(TaskStartedInfo) to all listener. |
boolean |
isAtLeastOneMacroRunning() |
AbstractProblemLoader |
load(Profile profile,
java.io.File file,
java.util.List<java.io.File> classPath,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
java.util.Properties poPropertiesToForce,
boolean forceNewProfileOfNewProofs)
Opens a java file in this
UserInterfaceControl and returns the instantiated AbstractProblemLoader
which can be used to instantiated proofs programmatically. |
void |
loadingFinished(AbstractProblemLoader loader,
IPersistablePO.LoadedPOContainer poContainer,
ProofAggregate proofList,
AbstractProblemLoader.ReplayResult result)
The loading has stopped.
|
void |
loadingStarted(AbstractProblemLoader loader)
The loading has started.
|
protected void |
macroFinished(ProofMacroFinishedInfo info) |
protected void |
macroStarted(TaskStartedInfo info) |
void |
proofCreated(ProblemInitializer sender,
ProofAggregate proofAggregate) |
void |
removeProverTaskListener(ProverTaskListener ptl)
Removes the given
ProverTaskListener . |
void |
taskFinished(TaskFinishedInfo info)
Called when a task is finished.
|
void |
taskProgress(int position)
Called when progress is made on a task.
|
void |
taskStarted(TaskStartedInfo info) |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getProofControl, getTermLabelVisibilityManager, registerProofAggregate
reportWarnings, selectProofObligation
progressStarted, progressStopped, reportException, reportStatus, reportStatus, resetStatus
setMaximum, setProgress
private int numOfInvokedMacros
private final java.util.List<ProverTaskListener> proverTaskListener
ProverTaskListener
.public void addProverTaskListener(ProverTaskListener ptl)
ProverTaskListener
which will be informed about all events.addProverTaskListener
in interface UserInterfaceControl
ptl
- The ProverTaskListener
to add.public void removeProverTaskListener(ProverTaskListener ptl)
ProverTaskListener
.removeProverTaskListener
in interface UserInterfaceControl
ptl
- The ProverTaskListener
to remove.protected void fireTaskStarted(TaskStartedInfo info)
ProverTaskListener.taskStarted(TaskStartedInfo)
to all listener.info
- the TaskStartedInfo
containing general information about the task that is just about to startprotected void fireTaskProgress(int position)
ProverTaskListener.taskProgress(int)
to all listener.position
- The current position.protected void fireTaskFinished(TaskFinishedInfo info)
ProverTaskListener.taskFinished(TaskFinishedInfo)
to all listener.info
- The TaskFinishedInfo
.public void taskStarted(TaskStartedInfo info)
taskStarted
in interface ProverTaskListener
public void taskProgress(int position)
ProverTaskListener
taskProgress
in interface ProverTaskListener
position
- indicates how much work has been done relative to the value of
size
passed in ProverTaskListener.taskStarted(TaskStartedInfo)
.public void taskFinished(TaskFinishedInfo info)
ProverTaskListener
taskFinished
in interface ProverTaskListener
info
- a TaskFinishedInfo object with additional informationpublic Proof createProof(InitConfig initConfig, ProofOblInput input) throws ProofInputException
Proof
in this UserInterfaceControl
for the given
ProofOblInput
based on the InitConfig
.createProof
in interface UserInterfaceControl
initConfig
- The InitConfig
which provides the source code.input
- The description of the Proof
to instantiate.Proof
.ProofInputException
- Occurred Exception.protected abstract ProofEnvironment createProofEnvironmentAndRegisterProof(ProofOblInput proofOblInput, ProofAggregate proofList, InitConfig initConfig)
proofOblInput
- the ProofOblInput
proofList
- the ProofAggregate
initConfig
- the InitConfig
to be usedProofEnvironment
where the ProofAggregate
has been registeredpublic void proofCreated(ProblemInitializer sender, ProofAggregate proofAggregate)
proofCreated
in interface ProblemInitializer.ProblemInitializerListener
public boolean isAtLeastOneMacroRunning()
protected void macroStarted(TaskStartedInfo info)
protected void macroFinished(ProofMacroFinishedInfo info)
public AbstractProblemLoader load(Profile profile, java.io.File file, java.util.List<java.io.File> classPath, java.io.File bootClassPath, java.util.List<java.io.File> includes, java.util.Properties poPropertiesToForce, boolean forceNewProfileOfNewProofs) throws ProblemLoaderException
Opens a java file in this UserInterfaceControl
and returns the instantiated AbstractProblemLoader
which can be used to instantiated proofs programmatically.
The loading is performed in the Thread
of the caller!
load
in interface UserInterfaceControl
profile
- An optional Profile
to use. If it is null
the default profile AbstractProfile.getDefaultProfile()
is used.file
- The java file to open.classPath
- The class path entries to use.bootClassPath
- The boot class path to use.includes
- Optional includes to consider.poPropertiesToForce
- Some optional Properties
for the PO which extend or overwrite saved PO Properties
.forceNewProfileOfNewProofs
- true
AbstractProblemLoader.profileOfNewProofs
will be used as
Profile
of new proofs, false
Profile
specified by problem file will be used for new proofs.AbstractProblemLoader
.ProblemLoaderException
- Occurred Exception.protected ProblemInitializer createProblemInitializer(Profile profile)
Creates a new ProblemInitializer
instance which is configured
for this UserInterfaceControl
.
This method is used by nearly all Eclipse based product that uses KeY.
profile
- The Profile
to use.ProblemInitializer
.public void loadingStarted(AbstractProblemLoader loader)
ProblemLoaderControl
loadingStarted
in interface ProblemLoaderControl
loader
- The source AbstractProblemLoader
.public void loadingFinished(AbstractProblemLoader loader, IPersistablePO.LoadedPOContainer poContainer, ProofAggregate proofList, AbstractProblemLoader.ReplayResult result) throws ProblemLoaderException
ProblemLoaderControl
loadingFinished
in interface ProblemLoaderControl
loader
- The source AbstractProblemLoader
.poContainer
- The loaded IPersistablePO.LoadedPOContainer
.proofList
- The created ProofAggregate
.result
- The occurred AbstractProblemLoader.ReplayResult
.ProblemLoaderException
- Occurred Exception.