public class ProofMacroWorker extends javax.swing.SwingWorker<ProofMacroFinishedInfo,java.lang.Void> implements InterruptListener
It decouples proof macros from the GUI event thread. It registers with the mediator to receive Stop-Button events
Modifier and Type | Field and Description |
---|---|
private java.lang.Exception |
exception
The thrown exception leading to cancellation of the task
|
private ProofMacroFinishedInfo |
info
The resulting information of the task or null if the task was cancelled an exception was thrown
|
private java.util.List<InteractionListener> |
interactionListeners |
private ProofMacro |
macro
The macro which is to be executed
|
private KeYMediator |
mediator
The mediator of the environment
|
private Node |
node
The
Node to start macro at. |
private PosInOccurrence |
posInOcc
This position may be null if no subterm selected
|
private static boolean |
SELECT_GOAL_AFTER_MACRO
This flag decides whether after a macro an open is selected or not.
|
Constructor and Description |
---|
ProofMacroWorker(Node node,
ProofMacro macro,
KeYMediator mediator,
PosInOccurrence posInOcc)
Instantiates a new proof macro worker.
|
Modifier and Type | Method and Description |
---|---|
void |
addInteractionListener(InteractionListener listener) |
protected ProofMacroFinishedInfo |
doInBackground() |
protected void |
done() |
protected void |
emitProofMacroFinished(Node node,
ProofMacro macro,
PosInOccurrence posInOcc,
ProofMacroFinishedInfo info) |
void |
interruptionPerformed() |
void |
removeInteractionListener(InteractionListener listener) |
private void |
selectOpenGoalBelow()
Select a goal below the currently selected node.
|
private static final boolean SELECT_GOAL_AFTER_MACRO
private final ProofMacro macro
private final KeYMediator mediator
private final PosInOccurrence posInOcc
private ProofMacroFinishedInfo info
private java.lang.Exception exception
private java.util.List<InteractionListener> interactionListeners
public ProofMacroWorker(Node node, ProofMacro macro, KeYMediator mediator, PosInOccurrence posInOcc)
node
- the Node
to start macro at.macro
- the macro, not nullmediator
- the mediator, not nullposInOcc
- the position, possibly nullprotected ProofMacroFinishedInfo doInBackground()
doInBackground
in class javax.swing.SwingWorker<ProofMacroFinishedInfo,java.lang.Void>
public void interruptionPerformed()
interruptionPerformed
in interface InterruptListener
protected void done()
done
in class javax.swing.SwingWorker<ProofMacroFinishedInfo,java.lang.Void>
protected void emitProofMacroFinished(Node node, ProofMacro macro, PosInOccurrence posInOcc, ProofMacroFinishedInfo info)
public void addInteractionListener(InteractionListener listener)
public void removeInteractionListener(InteractionListener listener)
private void selectOpenGoalBelow()