class TacletDescriber
extends java.lang.Object
InnerNodeView
. They compute the text to show for a rule application
which consists of the sequent including the applied rule.Constructor and Description |
---|
TacletDescriber() |
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
getTacletDescription(KeYMediator mediator,
Node node,
SequentPrintFilter filter)
Computes the text to show in this
JTextArea which consists of the
sequent including the applied rule. |
private static VisibleTermLabels |
getVisibleTermLabels() |
private static void |
writeSVModifiers(java.lang.StringBuffer out,
SchemaVariable sv) |
private static void |
writeTacletSchemaVariable(java.lang.StringBuffer out,
SchemaVariable schemaVar) |
private static void |
writeTacletSchemaVariablesHelper(java.lang.StringBuffer out,
Taclet t) |
private static void writeSVModifiers(java.lang.StringBuffer out, SchemaVariable sv)
private static void writeTacletSchemaVariable(java.lang.StringBuffer out, SchemaVariable schemaVar)
private static void writeTacletSchemaVariablesHelper(java.lang.StringBuffer out, Taclet t)
public static java.lang.String getTacletDescription(KeYMediator mediator, Node node, SequentPrintFilter filter)
Computes the text to show in this JTextArea
which consists of the
sequent including the applied rule.
This information is also relevant for other tools like the Symbolic Execution Debugger.
mediator
- The KeYMediator
to use.node
- The Node
to use.filter
- The SequentPrintFilter
to use.private static VisibleTermLabels getVisibleTermLabels()