de.uka.ilkd.key.control

Class DefaultProofControl

java.lang.Object

de.uka.ilkd.key.control.AbstractProofControl

de.uka.ilkd.key.control.DefaultProofControl

All Implemented Interfaces:

ProofControl

public class DefaultProofControl
extends AbstractProofControl

The default implementation of ProofControl.

Author:

Martin Hentschel

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	DefaultProofControl.AutoModeThread
private class	DefaultProofControl.MacroThread

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

AbstractProofControl.FocussedAutoModeTaskListener

Field Summary

Fields

Modifier and Type	Field and Description
private java.lang.Thread	autoModeThread The currently running Thread.
private UserInterfaceControl	ui The UserInterfaceControl in which this ProofControl is used.

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

interactionListeners

Constructor Summary

Constructors

Constructor and Description
DefaultProofControl(UserInterfaceControl ui, DefaultUserInterfaceControl defaultProverTaskListener) Constructor.
DefaultProofControl(UserInterfaceControl ui, DefaultUserInterfaceControl defaultProverTaskListener, RuleCompletionHandler ruleCompletionHandler) Constructor.

Method Summary

Modifier and Type	Method and Description
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.
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, fireAutoModeStarted, fireAutoModeStopped, getAppsForName, getAppsForName, getBuiltInRule, getBuiltInRuleApp, getBuiltInRuleAppsForName, getDefaultProverTaskListener, getFindTaclet, getNoFindTaclet, getRewriteTaclet, isAutoModeSupported, isMinimizeInteraction, pruneTo, pruneTo, removeAutoModeListener, removeInteractionListener, selectedBuiltInRule, selectedTaclet, 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 UserInterfaceControl ui

The UserInterfaceControl in which this ProofControl is used.

autoModeThread

private java.lang.Thread autoModeThread

The currently running Thread.

Constructor Detail

DefaultProofControl

public DefaultProofControl(UserInterfaceControl ui,
                           DefaultUserInterfaceControl defaultProverTaskListener)

Constructor.

Parameters:

ui - The UserInterfaceControl in which this ProofControl is used.

defaultProverTaskListener - The default ProverTaskListener which will be added to all started ApplyStrategy instances.

DefaultProofControl

public DefaultProofControl(UserInterfaceControl ui,
                           DefaultUserInterfaceControl defaultProverTaskListener,
                           RuleCompletionHandler ruleCompletionHandler)

Constructor.

Parameters:

ui - The UserInterfaceControl in which this ProofControl is used.

defaultProverTaskListener - The default ProverTaskListener which will be added to all started ApplyStrategy instances.

ruleCompletionHandler - An optional RuleCompletionHandler.

Method Detail

startAutoMode

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

Specified by:

startAutoMode in class AbstractProofControl

stopAutoMode

public void stopAutoMode()

Description copied from interface: ProofControl

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

waitWhileAutoMode

public void waitWhileAutoMode()

Description copied from interface: ProofControl

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

isInAutoMode

public boolean isInAutoMode()

Description copied from interface: ProofControl

Checks if the auto mode is currently running.

Returns:

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

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.