public class ProofMacroWorker extends SwingWorker<Void,Void> implements InterruptListener
SwingWorker.StateValue
Modifier and Type | Field and Description |
---|---|
private Exception |
exception
The thrown exception leading to cancellation of the task
|
private TaskFinishedInfo |
info
The resulting information of the task or null if the task was cancelled an exception was thrown
|
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 |
---|---|
protected Void |
doInBackground() |
protected void |
done() |
void |
interruptionPerformed() |
private void |
selectOpenGoalBelow() |
addPropertyChangeListener, cancel, execute, firePropertyChange, get, get, getProgress, getPropertyChangeSupport, getState, isCancelled, isDone, process, publish, removePropertyChangeListener, run, setProgress
private static final boolean SELECT_GOAL_AFTER_MACRO
private final ProofMacro macro
private TaskFinishedInfo info
private Exception exception
private final KeYMediator mediator
private final PosInOccurrence posInOcc
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 Void doInBackground() throws Exception
doInBackground
in class SwingWorker<Void,Void>
Exception
public void interruptionPerformed()
interruptionPerformed
in interface InterruptListener
protected void done()
done
in class SwingWorker<Void,Void>
private void selectOpenGoalBelow()