de.uka.ilkd.key.ui

Class AbstractMediatorUserInterfaceControl

java.lang.Object

de.uka.ilkd.key.control.AbstractUserInterfaceControl

de.uka.ilkd.key.ui.AbstractMediatorUserInterfaceControl

All Implemented Interfaces:

RuleCompletionHandler, UserInterfaceControl, ProofDisposedListener, ProblemInitializer.ProblemInitializerListener, ProblemLoaderControl, ProofEnvironmentListener, ProverTaskListener, ProgressMonitor, java.util.EventListener

Direct Known Subclasses:

ConsoleUserInterfaceControl, WindowUserInterfaceControl

public abstract class AbstractMediatorUserInterfaceControl
extends AbstractUserInterfaceControl
implements RuleCompletionHandler, ProofEnvironmentListener, ProofDisposedListener

Provides a basic implementation of UserInterfaceControl for user interfaces in which a KeYMediator is available.

Author:

Martin Hentschel

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 ProofMacro	autoMacro
private MediatorProofControl	proofControl
protected boolean	saveOnly

Constructor Summary

Constructors

Constructor and Description
AbstractMediatorUserInterfaceControl()

Method Summary

Modifier and Type	Method and Description
boolean	applyMacro()
boolean	confirmTaskRemoval(java.lang.String string) asks if removal of a task is completed.
protected MediatorProofControl	createProofControl()
ProofEnvironment	createProofEnvironmentAndRegisterProof(ProofOblInput proofOblInput, ProofAggregate proofList, InitConfig initConfig) registers the proof aggregate at the UI
ProofMacro	getMacro()
abstract KeYMediator	getMediator() Returns the used KeYMediator.
protected ProblemLoader	getProblemLoader(java.io.File file, java.util.List<java.io.File> classPath, java.io.File bootClassPath, java.util.List<java.io.File> includes, KeYMediator mediator)
MediatorProofControl	getProofControl() Returns the used ProofControl.
boolean	isSaveOnly()
abstract void	loadProblem(java.io.File file) loads the problem or proof from the given file
boolean	macroChosen()
protected void	macroFinished(ProofMacroFinishedInfo info)
protected void	macroSideProofDisposing(ProofMacroFinishedInfo initiatingInfo, Proof initiatingProof, Proof sideProof)
abstract void	notify(NotificationEvent event)
void	notifyAutoModeBeingStarted() these methods are called immediately before automode is started to ensure that the GUI can respond in a reasonable way, e.g., change the cursor to a waiting cursor
void	notifyAutomodeStopped() these methods are called when automode has been stopped to ensure that the GUI can respond in a reasonable way, e.g., change the cursor to the default
abstract void	openExamples() called to open the build in examples
void	proofDisposed(ProofDisposedEvent e) When a Proof was disposed via Proof.dispose().
void	proofDisposing(ProofDisposedEvent e) When a Proof is going to be disposed.
void	proofRegistered(ProofEnvironmentEvent event)
void	proofUnregistered(ProofEnvironmentEvent event)
void	registerProofAggregate(ProofAggregate pa) Registers an already created ProofAggregate in this UserInterfaceControl.
private void	saveSideProof(Proof proof) Try to save a side proof.
void	setMacro(ProofMacro macro)
void	setSaveOnly(boolean s)

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

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

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.RuleCompletionHandler

completeAndApplyTacletMatch, completeBuiltInRuleApp

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

getTermLabelVisibilityManager

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

saveOnly

protected boolean saveOnly

proofControl

private final MediatorProofControl proofControl

autoMacro

private ProofMacro autoMacro

Constructor Detail

AbstractMediatorUserInterfaceControl

public AbstractMediatorUserInterfaceControl()

Method Detail

getProofControl

public MediatorProofControl getProofControl()

Description copied from interface: UserInterfaceControl

Returns the used ProofControl.

Specified by:

getProofControl in interface UserInterfaceControl

Returns:

The used ProofControl.

createProofControl

protected MediatorProofControl createProofControl()

setSaveOnly

public void setSaveOnly(boolean s)

isSaveOnly

public boolean isSaveOnly()

setMacro

public void setMacro(ProofMacro macro)

getMacro

public ProofMacro getMacro()

macroChosen

public boolean macroChosen()

openExamples

public abstract void openExamples()

called to open the build in examples

getMediator

public abstract KeYMediator getMediator()

Returns the used KeYMediator.

Returns:

The used KeYMediator.

loadProblem

public abstract void loadProblem(java.io.File file)

loads the problem or proof from the given file

Parameters:

file - the File with the problem description or the proof

getProblemLoader

protected ProblemLoader getProblemLoader(java.io.File file,
                                         java.util.List<java.io.File> classPath,
                                         java.io.File bootClassPath,
                                         java.util.List<java.io.File> includes,
                                         KeYMediator mediator)

applyMacro

public boolean applyMacro()

macroFinished

protected void macroFinished(ProofMacroFinishedInfo info)

Overrides:

macroFinished in class AbstractUserInterfaceControl

macroSideProofDisposing

protected void macroSideProofDisposing(ProofMacroFinishedInfo initiatingInfo,
                                       Proof initiatingProof,
                                       Proof sideProof)

saveSideProof

private void saveSideProof(Proof proof)

Try to save a side proof. Saving does not rely on UI features, but failures are reported to the UI.

Parameters:

proof -

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

proofUnregistered

public void proofUnregistered(ProofEnvironmentEvent event)

Specified by:

proofUnregistered in interface ProofEnvironmentListener

notifyAutoModeBeingStarted

public void notifyAutoModeBeingStarted()

these methods are called immediately before automode is started to ensure that the GUI can respond in a reasonable way, e.g., change the cursor to a waiting cursor

notifyAutomodeStopped

public void notifyAutomodeStopped()

these methods are called when automode has been stopped to ensure that the GUI can respond in a reasonable way, e.g., change the cursor to the default

notify

public abstract void notify(NotificationEvent event)

confirmTaskRemoval

public boolean confirmTaskRemoval(java.lang.String string)

asks if removal of a task is completed. This is useful to display a dialog to the user and asking her or if on command line to allow it always.

Parameters:

message -

Returns:

true if removal has been granted

proofDisposing

public void proofDisposing(ProofDisposedEvent e)

When a Proof is going to be disposed.

Specified by:

proofDisposing in interface ProofDisposedListener

Parameters:

e - The event.

proofDisposed

public void proofDisposed(ProofDisposedEvent e)

When a Proof was disposed via Proof.dispose().

Specified by:

proofDisposed in interface ProofDisposedListener

Parameters:

e - The event.

proofRegistered

public void proofRegistered(ProofEnvironmentEvent event)

Specified by:

proofRegistered in interface ProofEnvironmentListener

registerProofAggregate

public void registerProofAggregate(ProofAggregate pa)

Registers an already created ProofAggregate in this UserInterfaceControl.

Specified by:

registerProofAggregate in interface UserInterfaceControl

Parameters:

pa - The ProofAggregate to register.