public abstract class SequentialProofMacro extends AbstractProofMacro
KeYMediator#startAutoMode()
.
Since ProofMacro
s run asynchronously, the start of the next macro
must be performed in a listener call at the end of a autostart.
ProofMacro.ProgressBarListener
Modifier and Type | Field and Description |
---|---|
private ProofMacro[] |
proofMacros
The proof macros to be applied in their order.
|
Constructor and Description |
---|
SequentialProofMacro() |
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.
|
boolean |
canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
|
protected abstract ProofMacro[] |
createProofMacroArray()
Creates the proof macro array.
|
java.util.List<ProofMacro> |
getProofMacros()
Gets the proof macros.
|
applyTo, canApplyTo, getMaxSteps, getScriptCommandName, hasParameter, resetParams, setParameter
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getCategory, getDescription, getName
private ProofMacro[] proofMacros
createProofMacroArray()
.protected abstract ProofMacro[] createProofMacroArray()
public boolean canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc)
This compound macro is applicable if and only if the first macro is applicable. If there is no first macro, this is not applicable.
proof
- the current Proof
(not null
)goals
- the goals (not null
)posInOcc
- the position in occurrence (may be null
)true
, if the macro is allowed to be appliedpublic 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.
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
public java.util.List<ProofMacro> getProofMacros()