public abstract class AlternativeMacro extends AbstractProofMacro
ProofMacro.ProgressBarListener
Modifier and Type | Field and Description |
---|---|
private ProofMacro[] |
proofMacros
The proof macro alternatives in their order according to their priority.
|
Constructor and Description |
---|
AlternativeMacro() |
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 any one of the macros 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 applicable macro of getProofMacros()
.
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 the macro is interrupted.java.lang.Exception
public java.util.List<ProofMacro> getProofMacros()