de.uka.ilkd.key.macros

Class SequentialOnLastGoalProofMacro

java.lang.Object

de.uka.ilkd.key.macros.AbstractProofMacro

de.uka.ilkd.key.macros.SequentialProofMacro

de.uka.ilkd.key.macros.SequentialOnLastGoalProofMacro

All Implemented Interfaces:

ProofMacro

public abstract class SequentialOnLastGoalProofMacro
extends SequentialProofMacro

Author:

christoph scheben

Nested Class Summary

Nested classes/interfaces inherited from interface de.uka.ilkd.key.macros.ProofMacro

ProofMacro.ProgressBarListener

Constructor Summary

Constructors

Constructor and Description
SequentialOnLastGoalProofMacro()

Method Summary

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.

Methods inherited from class de.uka.ilkd.key.macros.SequentialProofMacro

canApplyTo, createProofMacroArray, getProofMacros

Methods inherited from class de.uka.ilkd.key.macros.AbstractProofMacro

applyTo, canApplyTo, getMaxSteps, getScriptCommandName, hasParameter, resetParams, setParameter

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.macros.ProofMacro

getCategory, getDescription, getName

Constructor Detail

SequentialOnLastGoalProofMacro

public SequentialOnLastGoalProofMacro()

Method Detail

applyTo

public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic,
                                      Proof proof,
                                      ImmutableList<Goal> goals,
                                      PosInOccurrence posInOcc,
                                      ProverTaskListener listener)
                               throws java.lang.InterruptedException,
                                      java.lang.Exception

Apply this macro on the given goals. This method can change the proof by applying rules to it. This method is usually called from a dedicated thread and not the GUI thread. The thread it runs on may be interrupted. In this case, the macro may report the interruption by an 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 macro and registers a new AutoModeListener with the mediator. This listener unregisters itself after the last macro.

The macros are always started on the last active goal (in contrast to the same goal as it is done in the SequentialProofMacro).

Specified by:

applyTo in interface ProofMacro

Overrides:

applyTo in class SequentialProofMacro

Parameters:

uic - the UserInterfaceControl to use

proof - 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)

Throws:

java.lang.InterruptedException - if one of the wrapped macros is interrupted.

java.lang.Exception