| java.lang.Object
 de.uka.ilkd.key.pp.LogicPrinter
All known Subclasses: de.uka.ilkd.key.visualdebugger.DebuggerLP,
| LogicPrinter | | public class LogicPrinter (Code) | | The front end for the Sequent pretty-printer. It prints a sequent
and its parts and computes the PositionTable, which is needed for
highliting.
The actual layouting/formatting is done using the
de.uka.ilkd.key.util.pp.Layouter class. The concrete syntax for
operators is given by an instance of
NotationInfo . The
LogicPrinter is responsible for the concrete layout,
e.g. how terms with infix operators are indented, and it binds the
various needed components together.
See Also: NotationInfo
See Also: Notation
See Also: de.uka.ilkd.key.util.pp.Layouter |
| Constructor Summary | |
| public | LogicPrinter(ProgramPrinter prgPrinter, NotationInfo notationInfo, Services services)
Creates a LogicPrinter. | | public | LogicPrinter(ProgramPrinter prgPrinter, NotationInfo notationInfo, Backend backend, Services services)
Creates a LogicPrinter. | | public | LogicPrinter(ProgramPrinter prgPrinter, NotationInfo notationInfo, Services services, boolean purePrint)
Creates a LogicPrinter. | | public | LogicPrinter(ProgramPrinter prgPrinter, NotationInfo notationInfo, Backend backend, Services services, boolean purePrint)
Creates a LogicPrinter. |
| Method Summary | |
| public SVInstantiations | getInstantiations()
| | protected Layouter | getLayouter()
| | public NotationInfo | getNotationInfo()
| | public InitialPositionTable | getPositionTable()
returns the PositionTable representing position information on
the sequent of this LogicPrinter. | | protected Layouter | mark(Object o)
| | protected void | markEndSub()
Called after a substring is printed that has its own entry in a
position table. | | protected void | markStartSub()
Called before a substring is printed that has its own entry in
a position table. | | protected void | maybeParens(Term t, int ass)
Prints a subterm, if needed with parentheses. | | protected void | printAddProgVars(SetOfSchemaVariable apv)
| | public void | printAnonymousUpdate(Term t, int ass)
| | public void | printArray(String[] arraySep, Term t, int[] ass)
| | protected void | printAttribs(Taclet taclet)
| | public void | printCast(String pre, String post, Term t, int ass)
| | public void | printConstant(String s)
Print a constant. | | public void | printConstrainedFormula(ConstrainedFormula cfma)
Pretty-prints a constrained formula. | | public void | printConstraint(Constraint p)
Pretty-print a constraint
This does currently only work well for "EqualityConstraint"s,
which are printed as a list of unifications. | | protected void | printFind(Taclet taclet)
| | public void | printFunctionTerm(String name, Term t)
Print a term in f(t1,...tn) style. | | protected void | printGoalTemplate(TacletGoalTemplate tgt)
| | protected void | printGoalTemplates(Taclet taclet)
| | protected void | printHeuristic(RuleSet sv)
| | protected void | printHeuristics(Taclet taclet)
| | public void | printIfThenElseTerm(Term t, String keyword)
| | public boolean | printInShortForm(String attributeProgramName, Term t)
returns true if an attribute term shall be printed in short form. | | public boolean | printInShortForm(String programName, Sort sort)
| | public static boolean | printInShortForm(String programName, Sort sort, Services services)
| | public void | printInfixTerm(Term l, int assLeft, String name, Term r, int assRight)
Print a binary term in infix style. | | public void | printInfixTermContinuingBlock(Term l, int assLeft, String name, Term r, int assRight)
Print a binary term in infix style, continuing a containing
block. | | public void | printJavaBlock(JavaBlock j)
Print a Java block. | | public void | printLocationDescriptor(LocationDescriptor loc)
Pretty-prints a location descriptor. | | public void | printLocationDescriptors(SetOfLocationDescriptor locations)
Pretty-prints a set of location descriptors. | | public void | printMetavariable(Metavariable p_mv)
Prints a metavariable. | | public void | printModalityTerm(String left, JavaBlock jb, String right, Term phi, int ass)
Print a DL modality formula. | | protected void | printNewVarcond(NewVarcond sv)
| | protected void | printNotFreeIn(NotFreeIn sv)
| | public void | printOCLCollOpBoundVarTerm(Term collection, String arrow, String name, String leftParens, String iterVarDecl, String sep, Term expr, String rightParens)
Used for OCL Simplification. | | public void | printOCLCollOpTerm(String name, Term t)
Used for OCL Simplification. | | public void | printOCLCollectionTerm(Term t)
Used for OCL Simplification. | | public void | printOCLIfTerm(String ifS, Term ifT, String thenS, Term thenT, String elseS, Term elseT, String endif)
Used for OCL Simplification. | | public void | printOCLInvariantTerm(Term context, Term invariant)
Used for OCL Simplification. | | public void | printOCLIterateTerm(Term collection, String arrow, String name, String leftParens, String iterVarDecl, String sep1, String accVarDecl, String equals, Term accVarInit, String sep2, Term expr, String rightParens)
Used for OCL Simplification. | | public void | printOCLListOfInvariantsTerm(Term t)
Used for OCL Simplification. | | public void | printOCLUMLPropertyTerm(String name, Term t)
Used for OCL Simplification. | | public void | printOCLWrapperTerm(Term t)
Used for OCL Simplification. | | public void | printPostfixTerm(Term t, int ass, String name)
Print a unary term in postfix style. | | public void | printPrefixTerm(String name, Term t, int ass)
Print a unary term in prefix style. | | public void | printProgramElement(ProgramElement pe)
Pretty-prints a ProgramElement. | | public void | printProgramSV(ProgramSV pe)
Pretty-prints a ProgramSV. | | public void | printProgramVariable(ProgramVariable pv)
Pretty-Prints a ProgramVariable in the logic, not in Java blocks. | | public void | printQuanUpdateTerm(String l, String asgn, String r, Term t, int ass1, int ass2, int ass3)
Print a term with an (quantified) update. | | public void | printQuantifierTerm(String name, ArrayOfQuantifiableVariable vars, Term phi, int ass)
Print a quantified term. | | public void | printQueryTerm(String name, Term t, int ass)
Print a term in f(t1,...tn) style. | | protected void | printRewrite(Term t)
| | protected void | printRewriteAttributes(RewriteTaclet taclet)
| | protected void | printRules(ListOfTaclet rules)
| | protected void | printSchemaVariable(SchemaVariable sv)
| | public void | printSemisequent(Semisequent semiseq)
Pretty-prints a Semisequent. | | public void | printSemisequent(ListOfSequentPrintFilterEntry p_formulas)
| | public void | printSequent(Sequent seq, SequentPrintFilter filter, boolean finalbreak)
Pretty-print a sequent.
The sequent arrow is rendered as ==>. | | public void | printSequent(SequentPrintFilter filter, boolean finalbreak)
| | public void | printSequent(Sequent seq, boolean finalbreak)
| | public void | printSequent(Sequent seq, SequentPrintFilter filter)
Pretty-print a sequent.
The sequent arrow is rendered as =>. | | public void | printSequent(Sequent seq)
Pretty-print a sequent.
The sequent arrow is rendered as =>. | | public void | printShadowedAttribute(Term t1, int ass1, String name, Term t2)
| | public void | printSubstTerm(String l, QuantifiableVariable v, Term t, int ass2, String r, Term phi, int ass3)
Print a substitution term. | | public void | printTaclet(Taclet taclet, SVInstantiations sv, boolean showWholeTaclet)
Pretty-print a taclet. | | public void | printTaclet(Taclet taclet)
Pretty-print a taclet. | | public void | printTerm(Term t)
Pretty-prints a term or formula. | | public void | printTerm(ListOfTerm terms)
Pretty-prints a list of terms. | | public void | printTermContinuingBlock(Term t)
Pretty-prints a term or formula in the same block. | | protected void | printTextSequent(Sequent seq, String text, boolean frontbreak)
| | protected void | printVarCond(Taclet taclet)
| | protected void | printVariableCondition(VariableCondition sv)
| | public ProgramPrinter | programPrinter()
| | public static String | quickPrintLocationDescriptors(SetOfLocationDescriptor locations, Services services)
| | public void | reset()
Resets the Backend, the Layouter and (if applicable) the ProgramPrinter
of this Object. | | public StringBuffer | result()
Returns the pretty-printed sequent in a StringBuffer. | | public void | setInstantiation(SVInstantiations instantiations)
| | public int | setLineWidth(int lineWidth)
sets the line width to the new value but does not
reprint the sequent.
The actual set line width is the maximum of
LogicPrinter.DEFAULT_LINE_WIDTH and the given value
Parameters:
lineWidth - the max. | | String[] | setupUpdateSeparators(Operator loc, Term t)
| | protected void | startTerm(int size)
Start a term with subterms. | | public String | toString()
Returns the pretty-printed sequent. | | public void | update(Sequent seq, SequentPrintFilter filter, int lineWidth)
Reprints the sequent. |
| DEFAULT_LINE_WIDTH | | final public static int DEFAULT_LINE_WIDTH(Code) | | The default and minimal value o fthe
max. number of characters to put in one line
|
| formulaConstraint | | Constraint formulaConstraint(Code) | | The constraint used for metavariable instantiations of the
current formula
|
| logger | | static Logger logger(Code) | | |
| LogicPrinter | | public LogicPrinter(ProgramPrinter prgPrinter, NotationInfo notationInfo, Services services)(Code) | | Creates a LogicPrinter. Sets the sequent to be printed, as
well as a ProgramPrinter to print Java programs and a
NotationInfo which determines the concrete syntax.
Parameters:
prgPrinter - the ProgramPrinter that pretty-prints Java programs
Parameters:
notationInfo - the NotationInfo for the concrete syntax
Parameters:
services - The Services object |
| LogicPrinter | | public LogicPrinter(ProgramPrinter prgPrinter, NotationInfo notationInfo, Backend backend, Services services)(Code) | | Creates a LogicPrinter. Sets the sequent to be printed, as
well as a ProgramPrinter to print Java programs and a
NotationInfo which determines the concrete syntax.
Parameters:
prgPrinter - the ProgramPrinter that pretty-prints Java programs
Parameters:
notationInfo - the NotationInfo for the concrete syntax
Parameters:
backend - the Backend for the output
Parameters:
services - the Services object |
| LogicPrinter | | public LogicPrinter(ProgramPrinter prgPrinter, NotationInfo notationInfo, Services services, boolean purePrint)(Code) | | Creates a LogicPrinter. Sets the sequent to be printed, as
well as a ProgramPrinter to print Java programs and a
NotationInfo which determines the concrete syntax.
Parameters:
prgPrinter - the ProgramPrinter that pretty-prints Java programs
Parameters:
notationInfo - the NotationInfo for the concrete syntax
Parameters:
purePrint - if true the PositionTable will not be calculated(simulates the behaviour of the former PureSequentPrinter)
Parameters:
services - the Services object |
| LogicPrinter | | public LogicPrinter(ProgramPrinter prgPrinter, NotationInfo notationInfo, Backend backend, Services services, boolean purePrint)(Code) | | Creates a LogicPrinter. Sets the sequent to be printed, as
well as a ProgramPrinter to print Java programs and a
NotationInfo which determines the concrete syntax.
Parameters:
prgPrinter - the ProgramPrinter that pretty-prints Java programs
Parameters:
notationInfo - the NotationInfo for the concrete syntax
Parameters:
backend - the Backend for the output
Parameters:
purePrint - if true the PositionTable will not be calculated(simulates the behaviour of the former PureSequentPrinter) |
| getInstantiations | | public SVInstantiations getInstantiations()(Code) | | The SVInstantiations given with the last printTaclet call. |
| getLayouter | | protected Layouter getLayouter()(Code) | | Returns the Layouter
the Layouter |
| getNotationInfo | | public NotationInfo getNotationInfo()(Code) | | the notationInfo associated with this LogicPrinter |
| getPositionTable | | public InitialPositionTable getPositionTable()(Code) | | returns the PositionTable representing position information on
the sequent of this LogicPrinter. Subclasses may overwrite
this method with a null returning body if position information
is not computed there.
|
| markEndSub | | protected void markEndSub()(Code) | | Called after a substring is printed that has its own entry in a
position table. The backend will finishes the position table
on the top of the stack and set the entry on the top of the
stack to be the current position/position table. Subclasses may
overwrite this method with an empty body if position
information is not needed there.
|
| markStartSub | | protected void markStartSub()(Code) | | Called before a substring is printed that has its own entry in
a position table. The method sends a mark to the layouter,
which will make the backend set a start entry in posTbl, push a
new StackEntry with the current posTbl and current pos on the
stack and set the current pos to the length of the current
string result. Subclasses may overwrite this method with an
empty body if position information is not needed there.
|
| maybeParens | | protected void maybeParens(Term t, int ass) throws IOException(Code) | | Prints a subterm, if needed with parentheses. Each subterm has
a Priority. If the priority is less than the associativity for
that subterm fixed by the Notation/NotationInfo, parentheses
are needed.
If prio and associativity are equal, the subterm is printed
using
LogicPrinter.printTermContinuingBlock(Term) . This currently
only makes a difference for infix operators.
Parameters:
t - the the subterm to print
Parameters:
ass - the associativity for this subterm |
| printAddProgVars | | protected void printAddProgVars(SetOfSchemaVariable apv) throws IOException(Code) | | |
| printAnonymousUpdate | | public void printAnonymousUpdate(Term t, int ass) throws IOException(Code) | | prints an anonymous update
|
| printArray | | public void printArray(String[] arraySep, Term t, int[] ass) throws java.io.IOException(Code) | | Pretty-prints a (shadowed) array expression
Parameters:
arraySep - usually a [ and a ]
Parameters:
t - the array expression as a whole
Parameters:
ass - the associatives for the subterms |
| printConstant | | public void printConstant(String s) throws IOException(Code) | | Print a constant. This just prints the string s and
marks it as a nullary term.
Parameters:
s - the constant |
| printConstrainedFormula | | public void printConstrainedFormula(ConstrainedFormula cfma) throws IOException(Code) | | Pretty-prints a constrained formula. The constraint
"Constraint.BOTTOM" is suppressed
Parameters:
cfma - the constrained formula to be printed |
| printConstraint | | public void printConstraint(Constraint p) throws IOException(Code) | | Pretty-print a constraint
This does currently only work well for "EqualityConstraint"s,
which are printed as a list of unifications. The bottom
constraint doesn't get special handling in here, i.e. this
method should not be called for p == Constraint.BOTTOM
|
| printFunctionTerm | | public void printFunctionTerm(String name, Term t) throws IOException(Code) | | Print a term in f(t1,...tn) style. If the
operator has arity 0, no parentheses are printed, i.e.
f instead of f(). If the term
doesn't fit on one line, t2...tn are aligned below
t1.
Parameters:
name - the name to be printed before the parentheses.
Parameters:
t - the term to be printed. |
| printInShortForm | | public boolean printInShortForm(String attributeProgramName, Term t)(Code) | | returns true if an attribute term shall be printed in short form.
In opposite to the other printInShortForm methods
it takes care of meta variable instantiations
Parameters:
attributeProgramName - the String of the attribute's programname
Parameters:
t - the Term used as reference prefix true if an attribute term shall be printed in short form. |
| printInShortForm | | public boolean printInShortForm(String programName, Sort sort)(Code) | | tests if the program name together with the prefix sort
determines the attribute in a unique way
Parameters:
programName - the String denoting the program name ofthe attribute
Parameters:
sort - the ObjectSort in whose reachable hierarchywe test for uniqueness true if the attribute is uniquely determined |
| printInShortForm | | public static boolean printInShortForm(String programName, Sort sort, Services services)(Code) | | tests if the program name together with the prefix sort
determines the attribute in a unique way
Parameters:
programName - the String denoting the program name ofthe attribute
Parameters:
sort - the ObjectSort specifying the hierarchywhere to test for uniqueness
Parameters:
services - the Services class used to access the type hierarchy true if the attribute is uniquely determined |
| printInfixTerm | | public void printInfixTerm(Term l, int assLeft, String name, Term r, int assRight) throws IOException(Code) | | Print a binary term in infix style. For instance p
& q, where & is the infix
operator. If line breaks are necessary, the format is like
p
& q
The subterms are printed using
LogicPrinter.printTermContinuingBlock(Term) .
Parameters:
l - the left subterm
Parameters:
assLeft - associativity for left subterm
Parameters:
name - the infix operator
Parameters:
r - the right subterm
Parameters:
assRight - associativity for right subterm |
| printJavaBlock | | public void printJavaBlock(JavaBlock j) throws IOException(Code) | | Print a Java block. This is formatted using the ProgramPrinter
given to the constructor. The result is indented according to
the surrounding material. The first `executable' statement is
marked for highlighting.
Parameters:
j - the Java block to be printed |
| printLocationDescriptors | | public void printLocationDescriptors(SetOfLocationDescriptor locations) throws java.io.IOException(Code) | | Pretty-prints a set of location descriptors.
|
| printMetavariable | | public void printMetavariable(Metavariable p_mv) throws IOException(Code) | | Prints a metavariable. If the
LogicPrinter.formulaConstraint
contains an instantiation for the metavariable the instantiation
is printed rather than the metavariable itself.
Parameters:
p_mv - the Metavariable to be printed |
| printModalityTerm | | public void printModalityTerm(String left, JavaBlock jb, String right, Term phi, int ass) throws IOException(Code) | | Print a DL modality formula. phi is the whole
modality formula, not just the subformula inside the modality.
Normally, this looks like
<Program>psi, where psi = phi.sub(0).
No line breaks are inserted, as the program itself is always broken.
In case of a program modality with arity greater than 1,
the subformulae are listed between parens, like
<Program>(psi1,psi2)
|
| printOCLCollOpBoundVarTerm | | public void printOCLCollOpBoundVarTerm(Term collection, String arrow, String name, String leftParens, String iterVarDecl, String sep, Term expr, String rightParens) throws IOException(Code) | | Used for OCL Simplification.
Pretty-prints Collection operation expressions with one iteration variable.
"collection->forAll(elem:T | expr(elem))"
|
| printOCLCollOpTerm | | public void printOCLCollOpTerm(String name, Term t) throws IOException(Code) | | Used for OCL Simplification.
Pretty-prints Collection operation expressions without iteration variable.
"collection->includes(object)"
|
| printOCLCollectionTerm | | public void printOCLCollectionTerm(Term t) throws IOException(Code) | | Used for OCL Simplification.
Pretty-prints Collection expressions.
"Set{Alpha, Beta, Gamma}"
|
| printOCLInvariantTerm | | public void printOCLInvariantTerm(Term context, Term invariant) throws IOException(Code) | | Used for OCL Simplification.
Pretty-prints list of OCL constraints.
"context inv:
"
|
| printOCLIterateTerm | | public void printOCLIterateTerm(Term collection, String arrow, String name, String leftParens, String iterVarDecl, String sep1, String accVarDecl, String equals, Term accVarInit, String sep2, Term expr, String rightParens) throws IOException(Code) | | Used for OCL Simplification.
Pretty-prints iterate expressions.
"collection->iterate(elem:T1 ; acc:T2=init | expr(elem, acc))"
|
| printOCLListOfInvariantsTerm | | public void printOCLListOfInvariantsTerm(Term t) throws IOException(Code) | | Used for OCL Simplification.
Pretty-prints OCL constraints.
"context inv:
context inv:
"
|
| printOCLUMLPropertyTerm | | public void printOCLUMLPropertyTerm(String name, Term t) throws IOException(Code) | | Used for OCL Simplification.
Pretty-prints references to UML properties.
"self.queryMethod()"
|
| printOCLWrapperTerm | | public void printOCLWrapperTerm(Term t) throws IOException(Code) | | Used for OCL Simplification.
|
| printPostfixTerm | | public void printPostfixTerm(Term t, int ass, String name) throws IOException(Code) | | Print a unary term in postfix style. For instance
t.a, where .a is the postfix operator.
No line breaks are possible.
Parameters:
name - the postfix operator
Parameters:
t - the subterm to be printed
Parameters:
ass - the associativity for the subterm |
| printPrefixTerm | | public void printPrefixTerm(String name, Term t, int ass) throws IOException(Code) | | Print a unary term in prefix style. For instance
!a. No line breaks are possible.
Parameters:
name - the prefix operator
Parameters:
t - the subterm to be printed
Parameters:
ass - the associativity for the subterm |
| printProgramElement | | public void printProgramElement(ProgramElement pe) throws IOException(Code) | | Pretty-prints a ProgramElement.
Parameters:
pe - You've guessed it, the ProgramElement to be pretty-printed
throws:
IOException - |
| printProgramSV | | public void printProgramSV(ProgramSV pe) throws IOException(Code) | | Pretty-prints a ProgramSV.
Parameters:
pe - You've guessed it, the ProgramSV to be pretty-printed
throws:
IOException - |
| printProgramVariable | | public void printProgramVariable(ProgramVariable pv) throws IOException(Code) | | Pretty-Prints a ProgramVariable in the logic, not in Java blocks. Prints
out the full (logic) name, so if A.b is private, it becomes a.A::b .
Parameters:
pv - The ProgramVariable in the logic
throws:
IOException - |
| printQuanUpdateTerm | | public void printQuanUpdateTerm(String l, String asgn, String r, Term t, int ass1, int ass2, int ass3) throws IOException(Code) | | Print a term with an (quantified) update. This looks like
{loc1 := val1 || ... || locn := valn} t. If line breaks are necessary, the
format is
{loc1:=val1 || ... || locn:=valn}
t
Parameters:
l - the left brace
Parameters:
asgn - the assignment operator (including spaces)
Parameters:
r - the right brace
Parameters:
t - the update term
Parameters:
ass1 - associativity for the locations
Parameters:
ass2 - associativity for the new values
Parameters:
ass3 - associativity for phi |
| printQuantifierTerm | | public void printQuantifierTerm(String name, ArrayOfQuantifiableVariable vars, Term phi, int ass) throws IOException(Code) | | Print a quantified term. Normally, this looks like
all x:s.phi. If line breaks are necessary,
the format is
all x:s.
phi
Note that the parameter var has to contain the
variable name with colon and sort.
Parameters:
name - the name of the quantifier
Parameters:
var - the quantified variable (+colon and sort)
Parameters:
sep - the separator (usually a dot)
Parameters:
phi - the quantified formula
Parameters:
ass - associativity for phi |
| printQueryTerm | | public void printQueryTerm(String name, Term t, int ass) throws IOException(Code) | | Print a term in f(t1,...tn) style. If it doesn't
fit on one line, t2...tn are aligned below t1.
Print a term in o.q(t1,...tn) style.
Parameters:
name - the name of the query
Parameters:
t - the Term to be printed
Parameters:
ass - the int defining the associativity of the term |
| printSemisequent | | public void printSemisequent(Semisequent semiseq) throws IOException(Code) | | Pretty-prints a Semisequent. Formulae are separated by commas.
Parameters:
semiseq - the semisequent to be printed |
| printSemisequent | | public void printSemisequent(ListOfSequentPrintFilterEntry p_formulas) throws IOException(Code) | | |
| printSequent | | public void printSequent(Sequent seq, SequentPrintFilter filter, boolean finalbreak)(Code) | | Pretty-print a sequent.
The sequent arrow is rendered as ==>. If the
sequent doesn't fit in one line, a line break is inserted after each
formula, the sequent arrow is on a line of its own, and formulae
are indented w.r.t. the arrow.
Parameters:
seq - The Sequent to be pretty-printed
Parameters:
filter - The SequentPrintFilter for seq
Parameters:
finalbreak - Print an additional line-break at the end of the sequent. |
| printSequent | | public void printSequent(Sequent seq, boolean finalbreak)(Code) | | |
| printSequent | | public void printSequent(Sequent seq, SequentPrintFilter filter)(Code) | | Pretty-print a sequent.
The sequent arrow is rendered as =>. If the
sequent doesn't fit in one line, a line break is inserted after each
formula, the sequent arrow is on a line of its own, and formulae
are indented w.r.t. the arrow.
A line-break is printed after the Sequent.
Parameters:
seq - The Sequent to be pretty-printed
Parameters:
filter - The SequentPrintFilter for seq |
| printSequent | | public void printSequent(Sequent seq)(Code) | | Pretty-print a sequent.
The sequent arrow is rendered as =>. If the
sequent doesn't fit in one line, a line break is inserted after each
formula, the sequent arrow is on a line of its own, and formulae
are indented w.r.t. the arrow.
A line-break is printed after the Sequent.
No filtering is done.
Parameters:
seq - The Sequent to be pretty-printed |
| printShadowedAttribute | | public void printShadowedAttribute(Term t1, int ass1, String name, Term t2) throws java.io.IOException(Code) | | Pretty-prints a shadowed attribute
Parameters:
t1 - the attribute prefix
Parameters:
ass1 - the associativity for the reference prefix
Parameters:
name - the attribute name
Parameters:
t2 - the shadow number term |
| printSubstTerm | | public void printSubstTerm(String l, QuantifiableVariable v, Term t, int ass2, String r, Term phi, int ass3) throws IOException(Code) | | Print a substitution term. This looks like
{var/t}s. If line breaks are necessary, the
format is
{var/t}
s
Parameters:
l - the String used as left brace symbol
Parameters:
v - the QuantifiableVariable to be substituted
Parameters:
t - the Term to be used as new value
Parameters:
ass2 - the int defining the associativity for the new value
Parameters:
r - the String used as right brace symbol
Parameters:
phi - the substituted term/formula
Parameters:
ass3 - the int defining the associativity for phi |
| printTaclet | | public void printTaclet(Taclet taclet, SVInstantiations sv, boolean showWholeTaclet)(Code) | | Pretty-print a taclet. Line-breaks are taken care of.
Parameters:
taclet - The Taclet to be pretty-printed.
Parameters:
sv - The instantiations of the SchemaVariables
Parameters:
showWholeTaclet - Should the find, varcond and heuristic part be pretty-printed? |
| printTaclet | | public void printTaclet(Taclet taclet)(Code) | | Pretty-print a taclet. Line-breaks are taken care of. No instantiation is
applied.
Parameters:
taclet - The Taclet to be pretty-printed. |
| printTerm | | public void printTerm(Term t) throws IOException(Code) | | Pretty-prints a term or formula. How it is rendered depends on
the NotationInfo given to the constructor.
Parameters:
t - the Term to be printed |
| printTerm | | public void printTerm(ListOfTerm terms) throws IOException(Code) | | Pretty-prints a list of terms.
Parameters:
terms - the terms to be printed |
| printTermContinuingBlock | | public void printTermContinuingBlock(Term t) throws IOException(Code) | | Pretty-prints a term or formula in the same block. How it is
rendered depends on the NotationInfo given to the constructor.
`In the same block' means that no extra indentation will be
added if line breaks are necessary. A formula a & (b
& c) would print a & b & c, omitting
the redundant parentheses. The subformula b & c
is printed using this method to get a layout of
a
& b
& c
instead of
a
& b
& c
Parameters:
t - the Term to be printed |
| programPrinter | | public ProgramPrinter programPrinter()(Code) | | Returns the ProgramPrinter
the ProgramPrinter |
| quickPrintLocationDescriptors | | public static String quickPrintLocationDescriptors(SetOfLocationDescriptor locations, Services services)(Code) | | |
| reset | | public void reset()(Code) | | Resets the Backend, the Layouter and (if applicable) the ProgramPrinter
of this Object.
|
| result | | public StringBuffer result()(Code) | | Returns the pretty-printed sequent in a StringBuffer. This
should only be called after a printSequent invocation
returns.
the pretty-printed sequent. |
| setInstantiation | | public void setInstantiation(SVInstantiations instantiations)(Code) | | sets instantiations of schema variables
|
| setLineWidth | | public int setLineWidth(int lineWidth)(Code) | | sets the line width to the new value but does not
reprint the sequent.
The actual set line width is the maximum of
LogicPrinter.DEFAULT_LINE_WIDTH and the given value
Parameters:
lineWidth - the max. number of character to put on one line the actual set line width |
| startTerm | | protected void startTerm(int size)(Code) | | Start a term with subterms. The backend will set the current
posTbl to a newly created position table with the given number
of rows. Subclasses may overwrite this method with an empty
body if position information is not needed there.
Parameters:
size - the number of rows of the new position table |
| toString | | public String toString()(Code) | | Returns the pretty-printed sequent. This should only be called
after a printSequent invocation returns.
the pretty-printed sequent. |
| update | | public void update(Sequent seq, SequentPrintFilter filter, int lineWidth)(Code) | | Reprints the sequent. This can be useful if settings like
PresentationFeatures or abbreviations have changed.
Parameters:
seq - The Sequent to be reprinted
Parameters:
filter - The SequentPrintFilter for seq
Parameters:
lineWidth - the max. number of character to put on one line(the actual taken linewidth is the max ofLogicPrinter.DEFAULT_LINE_WIDTH and the given value |
|
|