de.uka.ilkd.key.control

Class DefaultUserInterfaceControl

java.lang.Object

de.uka.ilkd.key.control.AbstractUserInterfaceControl

de.uka.ilkd.key.control.DefaultUserInterfaceControl

All Implemented Interfaces:

UserInterfaceControl, ProblemInitializer.ProblemInitializerListener, ProblemLoaderControl, ProverTaskListener, ProgressMonitor

public class DefaultUserInterfaceControl
extends AbstractUserInterfaceControl

The DefaultUserInterfaceControl which allows proving in case that no specific user interface is available.

In case that no user interface should be used see also KeYEnvironment which provides static methods to load source code and to instantiate this class.

Author:

Martin Hentschel

See Also:

KeYEnvironment

Nested Class Summary

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

ProgressMonitor.Empty

Field Summary

Fields

Modifier and Type	Field and Description
private DefaultProofControl	proofControl The used DefaultProofControl.
private TermLabelVisibilityManager	termLabelVisibilityManager The used TermLabelVisibilityManager.

Constructor Summary

Constructors

Constructor and Description
DefaultUserInterfaceControl() Constructor.
DefaultUserInterfaceControl(RuleCompletionHandler customization) Constructor.

Method Summary

Modifier and Type	Method and Description
ProofEnvironment	createProofEnvironmentAndRegisterProof(ProofOblInput proofOblInput, ProofAggregate proofList, InitConfig initConfig) registers the proof aggregate at the UI
DefaultProofControl	getProofControl() Returns the used ProofControl.
TermLabelVisibilityManager	getTermLabelVisibilityManager() Returns the TermLabelVisibilityManager.
void	progressStarted(java.lang.Object sender)
void	progressStopped(java.lang.Object sender)
void	registerProofAggregate(ProofAggregate pa) Registers an already created ProofAggregate in this UserInterfaceControl.
void	reportException(java.lang.Object sender, ProofOblInput input, java.lang.Exception e)
void	reportStatus(java.lang.Object sender, java.lang.String status)
void	reportStatus(java.lang.Object sender, java.lang.String status, int progress)
void	reportWarnings(ImmutableSet<PositionedString> warnings) Report the occurred warnings.
void	resetStatus(java.lang.Object sender)
boolean	selectProofObligation(InitConfig initConfig) This method is called if no IPersistablePO.LoadedPOContainer was created via AbstractProblemLoader.createProofObligationContainer() and can be overwritten for instance to open the proof management dialog as done by ProblemLoader.
void	setMaximum(int maximum) Set the maximum number of steps for this task.
void	setProgress(int progress) Set the progress achieved so far.

Methods inherited from class de.uka.ilkd.key.control.AbstractUserInterfaceControl

addProverTaskListener, createProblemInitializer, createProof, fireTaskFinished, fireTaskProgress, fireTaskStarted, isAtLeastOneMacroRunning, load, loadingFinished, loadingStarted, macroFinished, macroStarted, proofCreated, removeProverTaskListener, taskFinished, taskProgress, taskStarted

Methods inherited from class java.lang.Object

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

Field Detail

termLabelVisibilityManager

private final TermLabelVisibilityManager termLabelVisibilityManager

The used TermLabelVisibilityManager.

proofControl

private final DefaultProofControl proofControl

The used DefaultProofControl.

Constructor Detail

DefaultUserInterfaceControl

public DefaultUserInterfaceControl()

Constructor.

DefaultUserInterfaceControl

public DefaultUserInterfaceControl(RuleCompletionHandler customization)

Constructor.

Parameters:

customization - An optional RuleCompletionHandler.

Method Detail

getProofControl

public DefaultProofControl getProofControl()

Returns the used ProofControl.

Returns:

The used ProofControl.

createProofEnvironmentAndRegisterProof

public ProofEnvironment createProofEnvironmentAndRegisterProof(ProofOblInput proofOblInput,
                                                               ProofAggregate proofList,
                                                               InitConfig initConfig)

registers the proof aggregate at the UI

Specified by:

createProofEnvironmentAndRegisterProof in class AbstractUserInterfaceControl

Parameters:

proofOblInput - the ProofOblInput

proofList - the ProofAggregate

initConfig - the InitConfig to be used

Returns:

the new ProofEnvironment where the ProofAggregate has been registered

selectProofObligation

public boolean selectProofObligation(InitConfig initConfig)

This method is called if no IPersistablePO.LoadedPOContainer was created via AbstractProblemLoader.createProofObligationContainer() and can be overwritten for instance to open the proof management dialog as done by ProblemLoader.

Returns:

true if the proof obligation was selected, and false if action was aborted

progressStarted

public void progressStarted(java.lang.Object sender)

progressStopped

public void progressStopped(java.lang.Object sender)

reportStatus

public void reportStatus(java.lang.Object sender,
                         java.lang.String status,
                         int progress)

reportStatus

public void reportStatus(java.lang.Object sender,
                         java.lang.String status)

resetStatus

public void resetStatus(java.lang.Object sender)

reportException

public void reportException(java.lang.Object sender,
                            ProofOblInput input,
                            java.lang.Exception e)

setProgress

public void setProgress(int progress)

Set the progress achieved so far. The parameter progress has to be >=0 and <= to the maximum value previously set with ProgressMonitor.setMaximum(int).

Parameters:

progress - number of steps completed

setMaximum

public void setMaximum(int maximum)

Set the maximum number of steps for this task.

Parameters:

maximum - maximum number of steps, >=0.

registerProofAggregate

public void registerProofAggregate(ProofAggregate pa)

Registers an already created ProofAggregate in this UserInterfaceControl.

Parameters:

pa - The ProofAggregate to register.

reportWarnings

public void reportWarnings(ImmutableSet<PositionedString> warnings)

Report the occurred warnings.

Parameters:

warnings - The occurred warnings.

getTermLabelVisibilityManager

public TermLabelVisibilityManager getTermLabelVisibilityManager()

Returns the TermLabelVisibilityManager.

Returns:

The TermLabelVisibilityManager.