public class SuccTacletBuilder extends FindTacletBuilder<SuccTaclet>
TacletBuilder.TacletBuilderException
Modifier and Type | Field and Description |
---|---|
private boolean |
ignoreTopLevelUpdates |
find
attrs, choices, goal2Choices, goals, ifseq, name, NONAME, ruleSets, taclet, tacletAnnotations, variableConditions, varsNew, varsNewDependingOn, varsNotFreeIn
Constructor and Description |
---|
SuccTacletBuilder() |
Modifier and Type | Method and Description |
---|---|
void |
addTacletGoalTemplate(TacletGoalTemplate goal)
adds a new goal descriptions to the goal descriptions of the Taclet.
|
SuccTaclet |
getSuccTaclet()
builds and returns the SuccTaclet that is specified by
former set... / add... methods.
|
SuccTaclet |
getTaclet()
builds and returns the Taclet that is specified by
former set... / add... methods.
|
SuccTacletBuilder |
setFind(Term findTerm)
sets the find of the Taclet that is to build to the given
term, if the sort of the given term is of Sort.FORMULA otherwise
nothing happens.
|
void |
setIgnoreTopLevelUpdates(boolean ignore) |
checkBoundInIfAndFind, getFind
addGoal2ChoicesMapping, addRuleSet, addVariableCondition, addVarsNew, addVarsNew, addVarsNew, addVarsNew, addVarsNewDependingOn, addVarsNotFreeIn, addVarsNotFreeIn, addVarsNotFreeIn, addVarsNotFreeIn, checkContainsFreeVarSV, checkContainsFreeVarSV, getChoices, getGoal2Choices, getName, getTacletWithoutInactiveGoalTemplates, goalTemplates, ifSequent, setAnnotations, setChoices, setDisplayName, setHelpText, setIfSequent, setName, setRuleSets, setTacletGoalTemplates, setTrigger, varsNotFreeIn
public SuccTacletBuilder setFind(Term findTerm)
public void addTacletGoalTemplate(TacletGoalTemplate goal)
addTacletGoalTemplate
in class TacletBuilder<SuccTaclet>
public SuccTaclet getSuccTaclet()
public SuccTaclet getTaclet()
getTaclet
in class TacletBuilder<SuccTaclet>
public void setIgnoreTopLevelUpdates(boolean ignore)