de.uka.ilkd.key.ui

Class MediatorProofControl

java.lang.Object

de.uka.ilkd.key.control.AbstractProofControl

de.uka.ilkd.key.ui.MediatorProofControl

All Implemented Interfaces:

ProofControl

public class MediatorProofControl
extends AbstractProofControl

A ProofControl which performs the automode in a SwingWorker.

Author:

Martin Hentschel

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	MediatorProofControl.AutoModeWorker

Nested classes/interfaces inherited from class de.uka.ilkd.key.control.AbstractProofControl

AbstractProofControl.FocussedAutoModeTaskListener

Field Summary

Fields

Modifier and Type	Field and Description
private AbstractMediatorUserInterfaceControl	ui
private MediatorProofControl.AutoModeWorker	worker

Fields inherited from class de.uka.ilkd.key.control.AbstractProofControl

interactionListeners

Constructor Summary

Constructors

Constructor and Description
MediatorProofControl(AbstractMediatorUserInterfaceControl ui)

Method Summary

Modifier and Type	Method and Description
void	fireAutoModeStarted(ProofEvent e) fires the event that automatic execution has started
void	fireAutoModeStopped(ProofEvent e) fires the event that automatic execution has stopped
boolean	isAutoModeSupported(Proof proof) Checks if the auto mode of this UserInterfaceControl supports the given Proof.
boolean	isInAutoMode() Checks if the auto mode is currently running.
void	runMacro(Node node, ProofMacro macro, PosInOccurrence posInOcc) Runs the given ProofMacro at the given PosInOccurrence on the given Node.
boolean	selectedTaclet(Taclet taclet, Goal goal, PosInOccurrence pos)
void	startAutoMode(Proof proof, ImmutableList<Goal> goals, ProverTaskListener ptl)
void	stopAutoMode() Requests to stop the current auto mode without blocking the current Thread until the auto mode has stopped.
void	waitWhileAutoMode() Blocks the current Thread while the auto mode of this UserInterfaceControl is active.

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

addAutoModeListener, addInteractionListener, applyInteractive, completeAndApplyApp, completeAndApplyTacletMatch, completeBuiltInRuleApp, completeBuiltInRuleAppByDefault, createModel, emitInteractivePrune, emitInteractiveRuleApplication, getAppsForName, getAppsForName, getBuiltInRule, getBuiltInRuleApp, getBuiltInRuleAppsForName, getDefaultProverTaskListener, getFindTaclet, getNoFindTaclet, getRewriteTaclet, isMinimizeInteraction, pruneTo, pruneTo, removeAutoModeListener, removeInteractionListener, selectedBuiltInRule, setMinimizeInteraction, startAndWaitForAutoMode, startAndWaitForAutoMode, startAutoMode, startAutoMode, startFocussedAutoMode, stopAndWaitAutoMode

Methods inherited from class java.lang.Object

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

Field Detail

ui

private final AbstractMediatorUserInterfaceControl ui

worker

private MediatorProofControl.AutoModeWorker worker

Constructor Detail

MediatorProofControl

public MediatorProofControl(AbstractMediatorUserInterfaceControl ui)

Method Detail

selectedTaclet

public boolean selectedTaclet(Taclet taclet,
                              Goal goal,
                              PosInOccurrence pos)

Specified by:

selectedTaclet in interface ProofControl

Overrides:

selectedTaclet in class AbstractProofControl

fireAutoModeStarted

public void fireAutoModeStarted(ProofEvent e)

Description copied from class: AbstractProofControl

fires the event that automatic execution has started

Overrides:

fireAutoModeStarted in class AbstractProofControl

fireAutoModeStopped

public void fireAutoModeStopped(ProofEvent e)

Description copied from class: AbstractProofControl

fires the event that automatic execution has stopped

Overrides:

fireAutoModeStopped in class AbstractProofControl

startAutoMode

public void startAutoMode(Proof proof,
                          ImmutableList<Goal> goals,
                          ProverTaskListener ptl)

Specified by:

startAutoMode in class AbstractProofControl

stopAutoMode

public void stopAutoMode()

Requests to stop the current auto mode without blocking the current Thread until the auto mode has stopped.

waitWhileAutoMode

public void waitWhileAutoMode()

Blocks the current Thread while the auto mode of this UserInterfaceControl is active.

isInAutoMode

public boolean isInAutoMode()

Checks if the auto mode is currently running.

Returns:

true auto mode is running, false auto mode is not running.

isAutoModeSupported

public boolean isAutoModeSupported(Proof proof)

Checks if the auto mode of this UserInterfaceControl supports the given Proof.

Specified by:

isAutoModeSupported in interface ProofControl

Overrides:

isAutoModeSupported in class AbstractProofControl

Parameters:

proof - The Proof to check.

Returns:

true auto mode support proofs, false auto mode don't support proof.

runMacro

public void runMacro(Node node,
                     ProofMacro macro,
                     PosInOccurrence posInOcc)

Runs the given ProofMacro at the given PosInOccurrence on the given Node.

Parameters:

node - The Node to start macro at.

macro - The ProofMacro to execute.

posInOcc - The exact PosInOccurrence at which the ProofMacro is started at.