de.uka.ilkd.key.rule

Enum Taclet.TacletLabelHint.TacletOperation

java.lang.Object

java.lang.Enum<Taclet.TacletLabelHint.TacletOperation>

de.uka.ilkd.key.rule.Taclet.TacletLabelHint.TacletOperation

All Implemented Interfaces:

java.io.Serializable, java.lang.Comparable<Taclet.TacletLabelHint.TacletOperation>

Enclosing class:

Taclet.TacletLabelHint

public static enum Taclet.TacletLabelHint.TacletOperation
extends java.lang.Enum<Taclet.TacletLabelHint.TacletOperation>

Defines the possible operations a Taclet performs.

Author:

Martin Hentschel

Enum Constant Summary

Enum Constants

Enum Constant and Description
ADD_ANTECEDENT Add clause of a Taclet applied to the antecedent.
ADD_SUCCEDENT Add clause of a Taclet applied to the succedent.
REPLACE_AT_ANTECEDENT Replace clause of a Taclet provides a Sequent and currently the current PosInOccurrence on the antecedent is modified.
REPLACE_AT_SUCCEDENT Replace clause of a Taclet provides a Sequent and currently the current PosInOccurrence on the succedent is modified.
REPLACE_TERM Replace clause of a Taclet provides a Term which is currently used to modify the PosInOccurrence.
REPLACE_TO_ANTECEDENT Replace clause of a Taclet provides a Sequent and currently additional adds to the antecedent are performed.
REPLACE_TO_SUCCEDENT Replace clause of a Taclet provides a Sequent and currently additional adds to the succedent are performed.

Method Summary

Modifier and Type	Method and Description
static Taclet.TacletLabelHint.TacletOperation	valueOf(java.lang.String name) Returns the enum constant of this type with the specified name.
static Taclet.TacletLabelHint.TacletOperation[]	values() Returns an array containing the constants of this enum type, in the order they are declared.

Methods inherited from class java.lang.Enum

clone, compareTo, equals, finalize, getDeclaringClass, hashCode, name, ordinal, toString, valueOf

Methods inherited from class java.lang.Object

getClass, notify, notifyAll, wait, wait, wait

Enum Constant Detail

ADD_ANTECEDENT

public static final Taclet.TacletLabelHint.TacletOperation ADD_ANTECEDENT

Add clause of a Taclet applied to the antecedent. Available information are Taclet.TacletLabelHint.getSequent() and Taclet.TacletLabelHint.getSequentFormula().

ADD_SUCCEDENT

public static final Taclet.TacletLabelHint.TacletOperation ADD_SUCCEDENT

Add clause of a Taclet applied to the succedent. Available information are Taclet.TacletLabelHint.getSequent() and Taclet.TacletLabelHint.getSequentFormula().

REPLACE_TO_ANTECEDENT

public static final Taclet.TacletLabelHint.TacletOperation REPLACE_TO_ANTECEDENT

Replace clause of a Taclet provides a Sequent and currently additional adds to the antecedent are performed. Available information are Taclet.TacletLabelHint.getSequent() and Taclet.TacletLabelHint.getSequentFormula().

REPLACE_AT_SUCCEDENT

public static final Taclet.TacletLabelHint.TacletOperation REPLACE_AT_SUCCEDENT

Replace clause of a Taclet provides a Sequent and currently the current PosInOccurrence on the succedent is modified. Available information are Taclet.TacletLabelHint.getSequent() and Taclet.TacletLabelHint.getSequentFormula().

REPLACE_AT_ANTECEDENT

public static final Taclet.TacletLabelHint.TacletOperation REPLACE_AT_ANTECEDENT

Replace clause of a Taclet provides a Sequent and currently the current PosInOccurrence on the antecedent is modified. Available information are Taclet.TacletLabelHint.getSequent() and Taclet.TacletLabelHint.getSequentFormula().

REPLACE_TO_SUCCEDENT

public static final Taclet.TacletLabelHint.TacletOperation REPLACE_TO_SUCCEDENT

Replace clause of a Taclet provides a Sequent and currently additional adds to the succedent are performed. Available information are Taclet.TacletLabelHint.getSequent() and Taclet.TacletLabelHint.getSequentFormula().

REPLACE_TERM

public static final Taclet.TacletLabelHint.TacletOperation REPLACE_TERM

Replace clause of a Taclet provides a Term which is currently used to modify the PosInOccurrence. Available information are Taclet.TacletLabelHint.getTerm().

Method Detail

values

public static Taclet.TacletLabelHint.TacletOperation[] values()

Returns an array containing the constants of this enum type, in the order they are declared. This method may be used to iterate over the constants as follows:

for (Taclet.TacletLabelHint.TacletOperation c : Taclet.TacletLabelHint.TacletOperation.values())
    System.out.println(c);

Returns:

an array containing the constants of this enum type, in the order they are declared

valueOf

public static Taclet.TacletLabelHint.TacletOperation valueOf(java.lang.String name)

Returns the enum constant of this type with the specified name. The string must match exactly an identifier used to declare an enum constant in this type. (Extraneous whitespace characters are not permitted.)

Parameters:

name - the name of the enum constant to be returned.

Returns:

the enum constant with the specified name

Throws:

java.lang.IllegalArgumentException - if this enum type has no constant with the specified name

java.lang.NullPointerException - if the argument is null