public abstract class SequentialOnLastGoalProofMacro extends SequentialProofMacro
ProofMacro.ProgressBarListener
Constructor and Description |
---|
SequentialOnLastGoalProofMacro() |
Modifier and Type | Method and Description |
---|---|
ProofMacroFinishedInfo |
applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener)
Apply this macro on the given goals.
|
canApplyTo, createProofMacroArray, getProofMacros
applyTo, canApplyTo, getMaxSteps, getScriptCommandName, hasParameter, resetParams, setParameter
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getCategory, getDescription, getName
public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc, ProverTaskListener listener) throws java.lang.InterruptedException, java.lang.Exception
InterruptedException
.
A ProverTaskListener
can be provided to which the progress will
be reported. If no reports are desired, null
cna be used for
this parameter. If more than one listener is needed, consider combining
them using a single listener object using the composite pattern.
This launches the first macro and registers a new
AutoModeListener
with the mediator
. This listener
unregisters itself after the last macro.
The macros are always started on the last active goal (in contrast to the same goal as it is done in the SequentialProofMacro).
applyTo
in interface ProofMacro
applyTo
in class SequentialProofMacro
uic
- the UserInterfaceControl
to useproof
- the current Proof
(not null
)goals
- the goals (not null
)posInOcc
- the position in occurrence (may be null
)listener
- the listener to use for progress reports (may be
null
)java.lang.InterruptedException
- if one of the wrapped macros is interrupted.java.lang.Exception