| java.lang.Object de.uka.ilkd.key.proof.TermTacletAppIndex
TermTacletAppIndex | public class TermTacletAppIndex (Code) | | Class whose objects represent an index of taclet apps for one particular
position within a formula, and that also contain references to the indices of
direct subformulas
|
Method Summary | |
public TermTacletAppIndex | addTaclets(RuleFilter filter, PosInOccurrence pos, Services services, Constraint userConstraint, TacletIndex tacletIndex, NewRuleListener listener) Create a new tree of indices that additionally contain the taclets that
are selected by filter
Parameters: filter - The taclets that are supposed to be added Parameters: pos - Pointer to the term/formula for which an index is tobe created. | public static TermTacletAppIndex | create(PosInOccurrence pos, Services services, Constraint userConstraint, TacletIndex tacletIndex, NewRuleListener listener, RuleFilter filter, TermTacletAppIndexCacheSet indexCaches) Create an index for the given term
Parameters: pos - Pointer to the term/formula for which an index is to becreated. | public static ListOfNoPosTacletApp | filter(RuleFilter p_filter, ListOfNoPosTacletApp taclets) | public ListOfNoPosTacletApp | getTacletAppAt(PosInOccurrence pos, RuleFilter p_filter) | public ListOfTacletApp | getTacletAppAtAndBelow(PosInOccurrence pos, RuleFilter filter) | public void | reportTacletApps(PosInOccurrence pos, NewRuleListener listener) Report all NoPosTacletApp s that are stored by
this (and by the sub-indices of this ). | public TermTacletAppIndex | update(PosInOccurrence pos, Services services, Constraint userConstraint, TacletIndex tacletIndex, NewRuleListener listener, TermTacletAppIndexCacheSet indexCaches) |
addTaclets | public TermTacletAppIndex addTaclets(RuleFilter filter, PosInOccurrence pos, Services services, Constraint userConstraint, TacletIndex tacletIndex, NewRuleListener listener)(Code) | | Create a new tree of indices that additionally contain the taclets that
are selected by filter
Parameters: filter - The taclets that are supposed to be added Parameters: pos - Pointer to the term/formula for which an index is tobe created. pos has to be a top-level termposition the index object |
filter | public static ListOfNoPosTacletApp filter(RuleFilter p_filter, ListOfNoPosTacletApp taclets)(Code) | | filtered list |
getTacletAppAtAndBelow | public ListOfTacletApp getTacletAppAtAndBelow(PosInOccurrence pos, RuleFilter filter)(Code) | | all taclet apps for or below the given position |
reportTacletApps | public void reportTacletApps(PosInOccurrence pos, NewRuleListener listener)(Code) | | Report all NoPosTacletApp s that are stored by
this (and by the sub-indices of this ).
Parameters: pos - The position of this index Parameters: listener - The listener to which the taclet apps found are supposed to bereported a list of all taclet apps |
|
|