de.uka.ilkd.key.proof.io

Interface ProblemLoaderControl

All Superinterfaces:

ProblemInitializer.ProblemInitializerListener, ProgressMonitor

All Known Implementing Classes:

AbstractMediatorUserInterfaceControl, AbstractUserInterfaceControl, ConsoleUserInterfaceControl, DefaultUserInterfaceControl, WindowUserInterfaceControl

public interface ProblemLoaderControl
extends ProblemInitializer.ProblemInitializerListener, ProgressMonitor

Allows to observe and control the loading performed by an AbstractProblemLoader.

Author:

Martin Hentschel

Nested Class Summary

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

ProgressMonitor.Empty

Method Summary

Modifier and Type	Method and Description
void	loadingFinished(AbstractProblemLoader loader, IPersistablePO.LoadedPOContainer poContainer, ProofAggregate proofList, AbstractProblemLoader.ReplayResult result) The loading has stopped.
void	loadingStarted(AbstractProblemLoader loader) The loading has started.
void	reportWarnings(ImmutableSet<PositionedString> warnings) Report the occurred warnings.
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.

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

progressStarted, progressStopped, proofCreated, reportException, reportStatus, reportStatus, resetStatus

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

setMaximum, setProgress

Method Detail

loadingStarted

void loadingStarted(AbstractProblemLoader loader)

The loading has started.

Parameters:

loader - The source AbstractProblemLoader.

loadingFinished

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

The loading has stopped.

Parameters:

loader - The source AbstractProblemLoader.

poContainer - The loaded IPersistablePO.LoadedPOContainer.

proofList - The created ProofAggregate.

result - The occurred AbstractProblemLoader.ReplayResult.

Throws:

ProblemLoaderException - Occurred Exception.

selectProofObligation

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

reportWarnings

void reportWarnings(ImmutableSet<PositionedString> warnings)

Report the occurred warnings.

Parameters:

warnings - The occurred warnings.