public class MediatorProofControl extends AbstractProofControl
ProofControl
which performs the automode in a SwingWorker
.Modifier and Type | Class and Description |
---|---|
private class |
MediatorProofControl.AutoModeWorker |
AbstractProofControl.FocussedAutoModeTaskListener
Modifier and Type | Field and Description |
---|---|
private AbstractMediatorUserInterfaceControl |
ui |
private MediatorProofControl.AutoModeWorker |
worker |
interactionListeners
Constructor and Description |
---|
MediatorProofControl(AbstractMediatorUserInterfaceControl ui) |
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)
|
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. |
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
private final AbstractMediatorUserInterfaceControl ui
private MediatorProofControl.AutoModeWorker worker
public MediatorProofControl(AbstractMediatorUserInterfaceControl ui)
public boolean selectedTaclet(Taclet taclet, Goal goal, PosInOccurrence pos)
selectedTaclet
in interface ProofControl
selectedTaclet
in class AbstractProofControl
public void fireAutoModeStarted(ProofEvent e)
AbstractProofControl
fireAutoModeStarted
in class AbstractProofControl
public void fireAutoModeStopped(ProofEvent e)
AbstractProofControl
fireAutoModeStopped
in class AbstractProofControl
public void startAutoMode(Proof proof, ImmutableList<Goal> goals, ProverTaskListener ptl)
startAutoMode
in class AbstractProofControl
public void stopAutoMode()
Thread
until the auto mode has stopped.public void waitWhileAutoMode()
Thread
while the auto mode of this
UserInterfaceControl
is active.public boolean isInAutoMode()
true
auto mode is running, false
auto mode is not running.public boolean isAutoModeSupported(Proof proof)
UserInterfaceControl
supports the given Proof
.isAutoModeSupported
in interface ProofControl
isAutoModeSupported
in class AbstractProofControl
proof
- The Proof
to check.true
auto mode support proofs, false
auto mode don't support proof.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.