public interface _LatexCTreeFormatter
Modifier and Type | Method and Description |
---|---|
java.lang.String |
format(_AbstractGoal node)
Returns the LaTeX translation of the spcified node set.
|
java.lang.String |
formatRuleName(_AbstractRule rule)
Returns the LaTeX translation of the name of the rule.
|
boolean |
generateFailureGoalAnnotations()
If it returns
true the generator will print details about
failed goals of C-tree. |
boolean |
generateNodeSetIndex()
If it returns
true the generator will index the node-sets
occurring in the C-Tree |
boolean |
generateRuleIndex()
If it returns
true the generator will index the rule
applications occurring in the C-Tree |
java.lang.String |
getIntro()
Returns the text to add at the beginning of the LaTeX document; this text
is added immediately after "
\begin{document} ". |
java.lang.String |
getPreamble()
Returns the text to add to the preamble of the LaTeX file; in general it
contains local macro definitions.
|
java.lang.String |
post(CTree ctree)
The LaTeX to insert after c-tree source.
|
java.lang.String |
pre(CTree ctree)
The LaTeX to insert before c-tree source or
null if no text is
to be inserted. |
LatexTranslator.ProofStyle |
proofStyle()
Returns the proof style to use.
|
LatexTranslator.ProofStyle proofStyle()
java.lang.String getPreamble()
java.lang.String getIntro()
\begin{document}
".java.lang.String format(_AbstractGoal node)
node
- the node set to translate.java.lang.String formatRuleName(_AbstractRule rule)
rule
- the rule.boolean generateNodeSetIndex()
true
the generator will index the node-sets
occurring in the C-Treetrue
if the node-sets must be numbered.boolean generateRuleIndex()
true
the generator will index the rule
applications occurring in the C-Treetrue
if the node-sets must be numbered.boolean generateFailureGoalAnnotations()
true
the generator will print details about
failed goals of C-tree.true
details about failed goals will be printed.java.lang.String pre(CTree ctree)
null
if no text is
to be inserted.ctree
- the c-tree.null
if no
text is to be inserted.java.lang.String post(CTree ctree)
ctree
- the c-treenull
if no
text is to be inserted..