public class DefaultProofControl extends AbstractProofControl
ProofControl
.Modifier and Type | Class and Description |
---|---|
private class |
DefaultProofControl.AutoModeThread |
private class |
DefaultProofControl.MacroThread |
AbstractProofControl.FocussedAutoModeTaskListener
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. |
interactionListeners
Constructor and Description |
---|
DefaultProofControl(UserInterfaceControl ui,
DefaultUserInterfaceControl defaultProverTaskListener)
Constructor.
|
DefaultProofControl(UserInterfaceControl ui,
DefaultUserInterfaceControl defaultProverTaskListener,
RuleCompletionHandler ruleCompletionHandler)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
boolean |
isInAutoMode()
Checks if the auto mode is currently running.
|
void |
runMacro(Node node,
ProofMacro macro,
PosInOccurrence posInOcc)
|
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. |
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
private final UserInterfaceControl ui
UserInterfaceControl
in which this ProofControl
is used.private java.lang.Thread autoModeThread
Thread
.public DefaultProofControl(UserInterfaceControl ui, DefaultUserInterfaceControl defaultProverTaskListener)
ui
- The UserInterfaceControl
in which this ProofControl
is used.defaultProverTaskListener
- The default ProverTaskListener
which will be added to all started ApplyStrategy
instances.public DefaultProofControl(UserInterfaceControl ui, DefaultUserInterfaceControl defaultProverTaskListener, RuleCompletionHandler ruleCompletionHandler)
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
.public void startAutoMode(Proof proof, ImmutableList<Goal> goals, ProverTaskListener ptl)
startAutoMode
in class AbstractProofControl
public void stopAutoMode()
ProofControl
Thread
until the auto mode has stopped.public void waitWhileAutoMode()
ProofControl
Thread
while the auto mode of this
UserInterfaceControl
is active.public boolean isInAutoMode()
ProofControl
true
auto mode is running, false
auto mode is not running.public void runMacro(Node node, ProofMacro macro, PosInOccurrence posInOcc)
node
- The Node
to start macro at.macro
- The ProofMacro
to execute.posInOcc
- The exact PosInOccurrence
at which the ProofMacro
is started at.