public class TryCloseMacro extends AbstractProofMacro
InteractiveProver$AutoWorker
.
Unlike many macros, this macros has got a parameter (numberSteps
), such
that several instances of the class may exist with different semantics.
The number of autosteps may be temporarily altered for this macro.Modifier and Type | Class and Description |
---|---|
private static class |
TryCloseMacro.TryCloseProgressBarListener |
ProofMacro.ProgressBarListener
Modifier and Type | Field and Description |
---|---|
private int |
numberSteps
The max number of steps to be applied.
|
Constructor and Description |
---|
TryCloseMacro()
Instantiates a new try close macro.
|
TryCloseMacro(int numberSteps)
Instantiates a new try close macro.
|
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?
|
java.lang.String |
getCategory()
Gets the category of this macro.
|
java.lang.String |
getDescription()
Gets the description of this macro.
|
java.lang.String |
getName()
Gets the name of this macro.
|
java.lang.String |
getScriptCommandName()
Gets a unique short name for this macro that can be used in proof
scripts.
|
private static ImmutableList<Goal> |
setDifference(ImmutableList<Goal> goals1,
ImmutableList<Goal> goals2) |
applyTo, canApplyTo, getMaxSteps, hasParameter, resetParams, setParameter
private final int numberSteps
public TryCloseMacro()
public TryCloseMacro(int numberSteps)
numberSteps
- the max number of steps. -1 means no change.public java.lang.String getName()
ProofMacro
null
constant stringpublic java.lang.String getScriptCommandName()
AbstractProofMacro
null
is returned, the macro cannot be addressed from
within scripts.
By default, proof macros do not support scripts, thus null
is returned.getScriptCommandName
in interface ProofMacro
getScriptCommandName
in class AbstractProofMacro
null
if not supported, or a non-null
constant string as the short namepublic java.lang.String getCategory()
ProofMacro
null
if no submenu is to be created.null
public java.lang.String getDescription()
ProofMacro
null
constant stringpublic boolean canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc)
ProofMacro
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
ProofMacro
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.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 application of the macro has been interrupted.private static ImmutableList<Goal> setDifference(ImmutableList<Goal> goals1, ImmutableList<Goal> goals2)