public interface ProofMacro
#canApplyTo(KeYMediator, PosInOccurrence)
). A macro is offered to the
user iff it returns true
. No changes should be made there.
A macro is then applied using #applyTo(KeYMediator, PosInOccurrence)
.
This may change the proof by applying rule applications. It is allowed to use
automatic runs, manual instantiations, ...
A proof macro needs to extract all necessary information on the application
from the mediator passed to the
#applyTo(KeYMediator, PosInOccurrence)
(or
#canApplyTo(KeYMediator, PosInOccurrence)
) method. You will be able
to access any interesting data from that starting point, especially
KeYMediator#getInteractiveProver()
.
KeYMediator
Modifier and Type | Interface and Description |
---|---|
static class |
ProofMacro.ProgressBarListener
This observer acts as intermediate instance between the reports by the
strategy and the UI reporting progress.
|
Modifier and Type | Method and Description |
---|---|
ProofMacroFinishedInfo |
applyTo(UserInterfaceControl uic,
Node node,
PosInOccurrence posInOcc,
ProverTaskListener listener)
Apply this macro on the given node.
|
ProofMacroFinishedInfo |
applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener)
Apply this macro on the given goals.
|
boolean |
canApplyTo(Node node,
PosInOccurrence posInOcc)
Can this macro be applied on the given node?
|
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.
|
boolean |
hasParameter(java.lang.String paramName)
Checks whether this
ProofMacro has a parameter named
paramName . |
void |
resetParams()
Resets the macro parameters to their defaults.
|
void |
setParameter(java.lang.String paramName,
java.lang.String paramValue)
Sets the parameter named
paramName to the given String
representation in paramValue . |
java.lang.String getName()
null
constant stringjava.lang.String getScriptCommandName()
null
is returned, the macro cannot be addressed from
within scripts.null
if not supported, or a non-null
constant string as the short namejava.lang.String getCategory()
null
if no submenu is to be created.null
java.lang.String getDescription()
null
constant stringboolean hasParameter(java.lang.String paramName)
ProofMacro
has a parameter named
paramName
. For use in proof scripts.paramName
- The name to check.ProofMacro
has a parameter named
paramName
.void setParameter(java.lang.String paramName, java.lang.String paramValue) throws java.lang.IllegalArgumentException
paramName
to the given String
representation in paramValue
. For use in proof scripts.paramName
- The name of the parameter.paramValue
- The value of the parameter.java.lang.IllegalArgumentException
- if there is no parameter of that name or the value is
incorrectly formatted (e.g., cannot be converted to a
number).void resetParams()
boolean canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc)
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 appliedboolean canApplyTo(Node node, PosInOccurrence posInOcc)
canApplyTo(Proof, ImmutableList, PosInOccurrence)
with
node.proof()
as proof and all open goals below
node
.node
- the node (not null
)posInOcc
- the position in occurrence (may be null
)true
, if the macro is allowed to be appliedProofMacroFinishedInfo 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.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.java.lang.Exception
ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Node node, 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
can 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 usenode
- the node (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.java.lang.Exception