public class TermTacletAppIndex
extends java.lang.Object
Modifier and Type | Method and Description |
---|---|
TermTacletAppIndex |
addTaclets(RuleFilter filter,
PosInOccurrence pos,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener)
Create a new tree of indices that additionally contain the taclets that
are selected by
filter |
static TermTacletAppIndex |
create(PosInOccurrence pos,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener,
RuleFilter filter,
TermTacletAppIndexCacheSet indexCaches)
Create an index for the given term
|
static ImmutableList<NoPosTacletApp> |
filter(RuleFilter p_filter,
ImmutableList<NoPosTacletApp> taclets) |
ImmutableList<NoPosTacletApp> |
getTacletAppAt(PosInOccurrence pos,
RuleFilter p_filter) |
ImmutableList<TacletApp> |
getTacletAppAtAndBelow(PosInOccurrence pos,
RuleFilter filter,
Services services) |
public static TermTacletAppIndex create(PosInOccurrence pos, Services services, TacletIndex tacletIndex, NewRuleListener listener, RuleFilter filter, TermTacletAppIndexCacheSet indexCaches)
pos
- Pointer to the term/formula for which an index is to be
created. pos
has to be a top-level term
positionpublic TermTacletAppIndex addTaclets(RuleFilter filter, PosInOccurrence pos, Services services, TacletIndex tacletIndex, NewRuleListener listener)
filter
filter
- The taclets that are supposed to be addedpos
- Pointer to the term/formula for which an index is to
be created. pos
has to be a top-level term
positionpublic ImmutableList<NoPosTacletApp> getTacletAppAt(PosInOccurrence pos, RuleFilter p_filter)
public ImmutableList<TacletApp> getTacletAppAtAndBelow(PosInOccurrence pos, RuleFilter filter, Services services)
public static ImmutableList<NoPosTacletApp> filter(RuleFilter p_filter, ImmutableList<NoPosTacletApp> taclets)
p_filter
- the RuleFilter
to be usedtaclets
- the list of Taclet
s to be filteredCopyright © 2003-2019 The KeY-Project.