de.uka.ilkd.key.control

Class AbstractUserInterfaceControl

java.lang.Object

de.uka.ilkd.key.control.AbstractUserInterfaceControl

All Implemented Interfaces:

UserInterfaceControl, ProblemInitializer.ProblemInitializerListener, ProblemLoaderControl, ProverTaskListener, ProgressMonitor

Direct Known Subclasses:

AbstractMediatorUserInterfaceControl, DefaultUserInterfaceControl

public abstract class AbstractUserInterfaceControl
extends java.lang.Object
implements UserInterfaceControl, ProblemLoaderControl, ProverTaskListener

Provides a basic implementation of UserInterfaceControl.

Author:

Martin Hentschel

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	AbstractUserInterfaceControl.ProofMacroListenerAdapter

Nested classes/interfaces inherited from interface de.uka.ilkd.key.util.ProgressMonitor

ProgressMonitor.Empty

Field Summary

Fields

Modifier and Type	Field and Description
private int	numOfInvokedMacros
private java.util.List<ProverTaskListener>	proverTaskListener The registered ProverTaskListener.

Constructor Summary

Constructors

Constructor and Description
AbstractUserInterfaceControl() Constructor.

Method Summary

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)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.control.UserInterfaceControl

getProofControl, getTermLabelVisibilityManager, registerProofAggregate

Methods inherited from interface de.uka.ilkd.key.proof.io.ProblemLoaderControl

reportWarnings, selectProofObligation

Methods inherited from interface de.uka.ilkd.key.proof.init.ProblemInitializer.ProblemInitializerListener

progressStarted, progressStopped, reportException, reportStatus, reportStatus, resetStatus

Methods inherited from interface de.uka.ilkd.key.util.ProgressMonitor

setMaximum, setProgress

Field Detail

numOfInvokedMacros

private int numOfInvokedMacros

proverTaskListener

private final java.util.List<ProverTaskListener> proverTaskListener

The registered ProverTaskListener.

Constructor Detail

AbstractUserInterfaceControl

public AbstractUserInterfaceControl()

Constructor.

Method Detail

addProverTaskListener

public void addProverTaskListener(ProverTaskListener ptl)

Registers the given ProverTaskListener which will be informed about all events.

Specified by:

addProverTaskListener in interface UserInterfaceControl

Parameters:

ptl - The ProverTaskListener to add.

removeProverTaskListener

public void removeProverTaskListener(ProverTaskListener ptl)

Removes the given ProverTaskListener.

Specified by:

removeProverTaskListener in interface UserInterfaceControl

Parameters:

ptl - The ProverTaskListener to remove.

fireTaskStarted

protected void fireTaskStarted(TaskStartedInfo info)

Fires the event ProverTaskListener.taskStarted(TaskStartedInfo) to all listener.

Parameters:

info - the TaskStartedInfo containing general information about the task that is just about to start

fireTaskProgress

protected void fireTaskProgress(int position)

Fires the event ProverTaskListener.taskProgress(int) to all listener.

Parameters:

position - The current position.

fireTaskFinished

protected void fireTaskFinished(TaskFinishedInfo info)

Fires the event ProverTaskListener.taskFinished(TaskFinishedInfo) to all listener.

Parameters:

info - The TaskFinishedInfo.

taskStarted

public void taskStarted(TaskStartedInfo info)

Specified by:

taskStarted in interface ProverTaskListener

taskProgress

public void taskProgress(int position)

Description copied from interface: ProverTaskListener

Called when progress is made on a task. This method is called after every single step of the task

Specified by:

taskProgress in interface ProverTaskListener

Parameters:

position - indicates how much work has been done relative to the value of size passed in ProverTaskListener.taskStarted(TaskStartedInfo).

taskFinished

public void taskFinished(TaskFinishedInfo info)

Description copied from interface: ProverTaskListener

Called when a task is finished.

Specified by:

taskFinished in interface ProverTaskListener

Parameters:

info - a TaskFinishedInfo object with additional information

createProof

public Proof createProof(InitConfig initConfig,
                         ProofOblInput input)
                  throws ProofInputException

Instantiates a new Proof in this UserInterfaceControl for the given ProofOblInput based on the InitConfig.

Specified by:

createProof in interface UserInterfaceControl

Parameters:

initConfig - The InitConfig which provides the source code.

input - The description of the Proof to instantiate.

Returns:

The instantiated Proof.

Throws:

ProofInputException - Occurred Exception.

createProofEnvironmentAndRegisterProof

protected abstract ProofEnvironment createProofEnvironmentAndRegisterProof(ProofOblInput proofOblInput,
                                                                           ProofAggregate proofList,
                                                                           InitConfig initConfig)

registers the proof aggregate at the UI

Parameters:

proofOblInput - the ProofOblInput

proofList - the ProofAggregate

initConfig - the InitConfig to be used

Returns:

the new ProofEnvironment where the ProofAggregate has been registered

proofCreated

public void proofCreated(ProblemInitializer sender,
                         ProofAggregate proofAggregate)

Specified by:

proofCreated in interface ProblemInitializer.ProblemInitializerListener

isAtLeastOneMacroRunning

public boolean isAtLeastOneMacroRunning()

macroStarted

protected void macroStarted(TaskStartedInfo info)

macroFinished

protected void macroFinished(ProofMacroFinishedInfo info)

load

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!

Specified by:

load in interface UserInterfaceControl

Parameters:

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.

Returns:

The opened AbstractProblemLoader.

Throws:

ProblemLoaderException - Occurred Exception.

createProblemInitializer

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.

Parameters:

profile - The Profile to use.

Returns:

The instantiated ProblemInitializer.

loadingStarted

public void loadingStarted(AbstractProblemLoader loader)

Description copied from interface: ProblemLoaderControl

The loading has started.

Specified by:

loadingStarted in interface ProblemLoaderControl

Parameters:

loader - The source AbstractProblemLoader.

loadingFinished

public void loadingFinished(AbstractProblemLoader loader,
                            IPersistablePO.LoadedPOContainer poContainer,
                            ProofAggregate proofList,
                            AbstractProblemLoader.ReplayResult result)
                     throws ProblemLoaderException

Description copied from interface: ProblemLoaderControl

The loading has stopped.

Specified by:

loadingFinished in interface ProblemLoaderControl

Parameters:

loader - The source AbstractProblemLoader.

poContainer - The loaded IPersistablePO.LoadedPOContainer.

proofList - The created ProofAggregate.

result - The occurred AbstractProblemLoader.ReplayResult.

Throws:

ProblemLoaderException - Occurred Exception.