Interface | Description |
---|---|
ChildTermLabelPolicy |
A
ChildTermLabelPolicy is used by
TermLabelManager#instantiateLabels(
TermLabelState, Services, PosInOccurrence, Term, Term, Rule, Goal,
Object, Term, Operator, ImmutableArray, ImmutableArray, JavaBlock)
to decide for each TermLabel on a child or grandchild of the
application Term if it should be re-added to the new Term
or not. |
RuleSpecificTask |
Instances of this class provides functionality only if a supported
rule is active.
|
TermLabelMerger |
A
TermLabelMerger is used by
TermLabelManager.mergeLabels(Services, de.uka.ilkd.key.logic.SequentChangeInfo)
to merge TermLabel s in case a SequentFormula was
rejected to be added to the resulting Sequent . |
TermLabelPolicy |
A
TermLabelPolicy is used by
TermLabelManager#instantiateLabels(
TermLabelState, Services, PosInOccurrence, Term, Term, Rule, Goal,
Object, Term, Operator, ImmutableArray, ImmutableArray, JavaBlock)
to decide for each TermLabel of an old Term if it
should be re-added to the new Term or not. |
TermLabelRefactoring |
A
TermLabelRefactoring is used by
TermLabelManager#refactorGoal(TermLabelState, Services, PosInOccurrence,
Term, Rule, Goal, Term)
to refactor the labels of each visited Term . |
TermLabelUpdate |
A
TermLabelUpdate is used by
TermLabelManager#instantiateLabels(
TermLabelState, Services, PosInOccurrence, Term, Term, Rule, Goal,
Object, Term, Operator, ImmutableArray, ImmutableArray, JavaBlock)
to add or remove maintained TermLabel s which will be added to the new Term . |
Enum | Description |
---|---|
TermLabelRefactoring.RefactoringScope |
Possible refactoring scopes.
|