public class LogicPrinter
extends java.lang.Object
The actual layouting/formatting is done using the 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.
NotationInfo
,
Notation
,
Layouter
Modifier and Type | Class and Description |
---|---|
private static class |
LogicPrinter.MarkType |
private static class |
LogicPrinter.PosTableStringBackend
A
Backend which puts its
result in a StringBuffer and builds a PositionTable. |
private static class |
LogicPrinter.QuantifiableVariablePrintMode |
private static class |
LogicPrinter.StackEntry
Utility class for stack entries containing the position table
and the position of the start of the subterm in the result.
|
Modifier and Type | Field and Description |
---|---|
private Backend |
backend
The backend
layouter will write to. |
private boolean |
createPositionTable |
static int |
DEFAULT_LINE_WIDTH
The default and minimal value of the
max. number of characters to put in one line
|
private SVInstantiations |
instantiations |
protected Layouter |
layouter
This chooses the layout.
|
private int |
lineWidth
The max. number of characters to put in one line
|
protected NotationInfo |
notationInfo
Contains information on the concrete syntax of operators.
|
private ProgramPrinter |
prgPrinter
The ProgramPrinter used to pretty-print Java blocks in
formulae.
|
private boolean |
pure
If pure is true the PositionTable will not be calculated
|
private LogicPrinter.QuantifiableVariablePrintMode |
quantifiableVariablePrintMode |
private SelectPrinter |
selectPrinter |
protected Services |
services
the services object
|
private StorePrinter |
storePrinter |
Constructor and Description |
---|
LogicPrinter(ProgramPrinter prgPrinter,
NotationInfo notationInfo,
Backend backend,
Services services,
boolean purePrint)
Creates a LogicPrinter.
|
LogicPrinter(ProgramPrinter prgPrinter,
NotationInfo notationInfo,
Services services)
Creates a LogicPrinter.
|
LogicPrinter(ProgramPrinter prgPrinter,
NotationInfo notationInfo,
Services services,
boolean purePrint)
Creates a LogicPrinter.
|
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
escapeHTML(java.lang.String text,
boolean escapeWhitespace)
escapes special characters by their HTML encoding
|
protected HeapLDT |
getHeapLDT() |
InitialPositionTable |
getInitialPositionTable()
returns the PositionTable representing position information on
the sequent of this LogicPrinter.
|
SVInstantiations |
getInstantiations() |
protected Layouter |
getLayouter()
Returns the Layouter
|
NotationInfo |
getNotationInfo() |
PositionTable |
getPositionTable()
returns the PositionTable representing position information on
the sequent of this LogicPrinter.
|
protected ImmutableArray<TermLabel> |
getVisibleTermLabels(Term t)
Determine the Set of labels that will be printed out for a specific
Term . |
protected Layouter |
mark(LogicPrinter.MarkType type) |
protected Layouter |
mark(LogicPrinter.MarkType type,
int parameter) |
protected void |
markEndJavaBlock()
Called after java block is printed and marks current position.
|
protected void |
markEndKeyword()
Called after keyword is printed and marks current position.
|
protected void |
markEndSub()
Called after a substring is printed that has its own entry in a
position table.
|
protected void |
markStartJavaBlock()
Called before java block is printed and marks current position.
|
protected void |
markStartKeyword()
Called before keyword is printed and marks current position.
|
protected void |
markStartSub()
Called before a substring is printed that has its own entry in
a position table.
|
protected void |
markStartSub(int subterm)
TODO
|
protected void |
maybeParens(Term t,
int ass)
Prints a subterm, if needed with parentheses.
|
protected void |
printAddProgVars(ImmutableSet<SchemaVariable> apv) |
protected void |
printAttribs(Taclet taclet) |
void |
printCast(java.lang.String pre,
java.lang.String post,
Term t,
int ass) |
void |
printClassName(java.lang.String className) |
void |
printConstant(java.lang.String s)
Print a constant.
|
void |
printConstant(Term t,
java.lang.String s)
Print a constant.
|
void |
printConstrainedFormula(SequentFormula cfma)
Pretty-prints a constrained formula.
|
protected void |
printDisplayName(Taclet taclet) |
void |
printElementaryUpdate(java.lang.String asgn,
Term t,
int ass2)
Print an elementary update.
|
void |
printElementOf(Term t) |
void |
printElementOf(Term t,
java.lang.String symbol) |
protected boolean |
printEmbeddedHeapConstructorTerm(Term t) |
protected void |
printEmbeddedObserver(Term heapTerm,
Term objectTerm) |
protected void |
printFind(Taclet taclet) |
void |
printFunctionTerm(Term t)
Print a term in
f(t1,...tn) style. |
protected void |
printGoalTemplate(TacletGoalTemplate tgt) |
protected void |
printGoalTemplates(Taclet taclet) |
void |
printHeapConstructor(Term t,
boolean closingBrace) |
protected void |
printHeuristic(RuleSet sv) |
protected void |
printHeuristics(Taclet taclet) |
void |
printIfThenElseTerm(Term t,
java.lang.String keyword) |
void |
printInfixTerm(Term l,
int assLeft,
java.lang.String name,
Term t,
Term r,
int assRight)
Print a binary term in infix style.
|
void |
printInfixTermContinuingBlock(Term l,
int assLeft,
java.lang.String name,
Term t,
Term r,
int assRight)
Print a binary term in infix style, continuing a containing
block.
|
boolean |
printInShortForm(java.lang.String programName,
Sort sort)
tests if the program name together with the prefix sort
determines the attribute in a unique way
|
static boolean |
printInShortForm(java.lang.String programName,
Sort sort,
Services services)
tests if the program name together with the prefix sort
determines the attribute in a unique way
|
boolean |
printInShortForm(java.lang.String attributeProgramName,
Term t)
returns true if an attribute term shall be printed in short form.
|
void |
printJavaBlock(JavaBlock j)
Print a Java block.
|
void |
printLabels(Term t) |
(package private) void |
printLabels(Term t,
java.lang.String left,
java.lang.String right) |
private void |
printMarkingFirstStatement(java.lang.String s,
Range r,
Range[] keywords)
Print a string marking a range as first statement.
|
void |
printModalityTerm(java.lang.String left,
JavaBlock jb,
java.lang.String right,
Term phi,
int ass)
Print a DL modality formula.
|
protected void |
printNewVarcond(NewVarcond sv) |
private void |
printNewVarDepOnCond(NewDependingOn on) |
protected void |
printNotFreeIn(NotFreeIn sv) |
void |
printObserver(Term t,
Term tacitHeap) |
void |
printParallelUpdate(java.lang.String separator,
Term t,
int ass) |
private void |
printParallelUpdateHelper(java.lang.String separator,
Term t,
int ass) |
void |
printPostfix(Term t,
java.lang.String postfix) |
void |
printPostfixTerm(Term t,
int ass,
java.lang.String name)
Print a unary term in postfix style.
|
void |
printPrefixTerm(java.lang.String name,
Term t,
Term sub,
int ass)
Print a unary term in prefix style.
|
void |
printProgramElement(ProgramElement pe)
Pretty-prints a ProgramElement.
|
void |
printProgramSV(ProgramSV pe)
Pretty-prints a ProgramSV.
|
void |
printProgramVariable(ProgramVariable pv)
Pretty-Prints a ProgramVariable in the logic, not in Java blocks.
|
void |
printQuantifierTerm(java.lang.String name,
ImmutableArray<QuantifiableVariable> vars,
Term phi,
int ass)
Print a quantified term.
|
protected void |
printRewrite(Term t) |
protected void |
printRewriteAttributes(RewriteTaclet taclet) |
protected void |
printRules(ImmutableList<Taclet> rules) |
protected void |
printSchemaVariable(SchemaVariable sv) |
void |
printSelect(Term t,
Term tacitHeap) |
void |
printSemisequent(ImmutableList<SequentPrintFilterEntry> p_formulas) |
void |
printSemisequent(Semisequent semiseq)
Pretty-prints a Semisequent.
|
void |
printSeqGet(Term t) |
void |
printSeqSingleton(Term t,
java.lang.String lDelimiter,
java.lang.String rDelimiter) |
void |
printSequent(Sequent seq)
Pretty-print a sequent.
|
void |
printSequent(Sequent seq,
boolean finalbreak) |
void |
printSequent(SequentPrintFilter filter)
Pretty-print a sequent.
|
void |
printSequent(SequentPrintFilter filter,
boolean finalbreak) |
void |
printSingleton(Term t) |
void |
printStore(Term t,
boolean closingBrace) |
void |
printSubstTerm(java.lang.String l,
QuantifiableVariable v,
Term t,
int ass2,
java.lang.String r,
Term phi,
int ass3)
Print a substitution term.
|
void |
printTaclet(Taclet taclet)
Pretty-print a taclet.
|
void |
printTaclet(Taclet taclet,
SVInstantiations sv,
boolean showWholeTaclet,
boolean declareSchemaVars)
Pretty-print a taclet.
|
void |
printTerm(ImmutableSet<Term> terms)
Pretty-prints a set of terms.
|
void |
printTerm(Term t)
Pretty-prints a term or formula.
|
void |
printTermContinuingBlock(Term t)
Pretty-prints a term or formula in the same block.
|
protected void |
printTextSequent(Sequent seq,
java.lang.String text,
boolean frontbreak) |
void |
printUpdateApplicationTerm(java.lang.String l,
java.lang.String r,
Term t,
int ass3)
Print a term with an update.
|
protected void |
printVarCond(Taclet taclet) |
protected void |
printVariableCondition(VariableCondition sv) |
private void |
printVariables(ImmutableArray<QuantifiableVariable> vars,
LogicPrinter.QuantifiableVariablePrintMode mode) |
private void |
printVerbatim(java.lang.String s)
Print a string containing newlines to the layouter.
|
ProgramPrinter |
programPrinter()
Returns the ProgramPrinter
|
static java.lang.String |
quickPrintSemisequent(Semisequent s,
Services services) |
static java.lang.String |
quickPrintSequent(Sequent s,
Services services) |
static java.lang.String |
quickPrintTerm(Term t,
Services services) |
static java.lang.String |
quickPrintTerm(Term t,
Services services,
boolean usePrettyPrinting,
boolean useUnicodeSymbols) |
void |
reset()
Resets the Backend, the Layouter and (if applicable) the ProgramPrinter
of this Object.
|
java.lang.StringBuffer |
result()
Returns the pretty-printed sequent in a StringBuffer.
|
void |
setInstantiation(SVInstantiations instantiations)
sets instantiations of schema variables
|
int |
setLineWidth(int lineWidth)
sets the line width to the new value but does not
reprint the sequent.
|
protected void |
startTerm(int size)
Start a term with subterms.
|
java.lang.String |
toString()
Returns the pretty-printed sequent.
|
void |
update(SequentPrintFilter filter,
int lineWidth)
Reprints the sequent.
|
public static final int DEFAULT_LINE_WIDTH
private int lineWidth
private final ProgramPrinter prgPrinter
protected final NotationInfo notationInfo
protected final Services services
protected Layouter layouter
private Backend backend
layouter
will write to.private boolean pure
private SVInstantiations instantiations
private final SelectPrinter selectPrinter
private final StorePrinter storePrinter
private LogicPrinter.QuantifiableVariablePrintMode quantifiableVariablePrintMode
private final boolean createPositionTable
public LogicPrinter(ProgramPrinter prgPrinter, NotationInfo notationInfo, Backend backend, Services services, boolean purePrint)
prgPrinter
- the ProgramPrinter that pretty-prints Java programsnotationInfo
- the NotationInfo for the concrete syntaxbackend
- the Backend for the outputpurePrint
- if true the PositionTable will not be calculated
(simulates the behaviour of the former PureSequentPrinter)public LogicPrinter(ProgramPrinter prgPrinter, NotationInfo notationInfo, Services services)
prgPrinter
- the ProgramPrinter that pretty-prints Java programsnotationInfo
- the NotationInfo for the concrete syntaxservices
- The Services objectpublic LogicPrinter(ProgramPrinter prgPrinter, NotationInfo notationInfo, Services services, boolean purePrint)
prgPrinter
- the ProgramPrinter that pretty-prints Java programsnotationInfo
- the NotationInfo for the concrete syntaxpurePrint
- if true the PositionTable will not be calculated
(simulates the behaviour of the former PureSequentPrinter)services
- the Services objectprotected HeapLDT getHeapLDT()
public static java.lang.String quickPrintTerm(Term t, Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols)
public static java.lang.String quickPrintSemisequent(Semisequent s, Services services)
public NotationInfo getNotationInfo()
public void reset()
public int setLineWidth(int lineWidth)
DEFAULT_LINE_WIDTH
and the given valuelineWidth
- the max. number of character to put on one linepublic void update(SequentPrintFilter filter, int lineWidth)
filter
- The SequentPrintFilter for seqlineWidth
- the max. number of character to put on one line
(the actual taken linewidth is the max of
DEFAULT_LINE_WIDTH
and the given valuepublic void setInstantiation(SVInstantiations instantiations)
public void printTaclet(Taclet taclet, SVInstantiations sv, boolean showWholeTaclet, boolean declareSchemaVars)
taclet
- The Taclet to be pretty-printed.sv
- The instantiations of the SchemaVariablesshowWholeTaclet
- Should the find, varcond and heuristic part be pretty-printed?declareSchemaVars
- Should declarations for the schema variables used in the taclet be pretty-printed?public void printTaclet(Taclet taclet)
taclet
- The Taclet to be pretty-printed.protected void printAttribs(Taclet taclet) throws java.io.IOException
java.io.IOException
protected void printDisplayName(Taclet taclet) throws java.io.IOException
java.io.IOException
protected void printRewriteAttributes(RewriteTaclet taclet) throws java.io.IOException
java.io.IOException
protected void printVarCond(Taclet taclet) throws java.io.IOException
java.io.IOException
private void printNewVarDepOnCond(NewDependingOn on) throws java.io.IOException
java.io.IOException
protected void printNewVarcond(NewVarcond sv) throws java.io.IOException
java.io.IOException
protected void printNotFreeIn(NotFreeIn sv) throws java.io.IOException
java.io.IOException
protected void printVariableCondition(VariableCondition sv) throws java.io.IOException
java.io.IOException
protected void printHeuristics(Taclet taclet) throws java.io.IOException
java.io.IOException
protected void printHeuristic(RuleSet sv) throws java.io.IOException
java.io.IOException
protected void printFind(Taclet taclet) throws java.io.IOException
java.io.IOException
protected void printTextSequent(Sequent seq, java.lang.String text, boolean frontbreak) throws java.io.IOException
java.io.IOException
protected void printGoalTemplates(Taclet taclet) throws java.io.IOException
java.io.IOException
protected void printGoalTemplate(TacletGoalTemplate tgt) throws java.io.IOException
java.io.IOException
protected void printRules(ImmutableList<Taclet> rules) throws java.io.IOException
java.io.IOException
protected void printAddProgVars(ImmutableSet<SchemaVariable> apv) throws java.io.IOException
java.io.IOException
protected void printSchemaVariable(SchemaVariable sv) throws java.io.IOException
java.io.IOException
public void printProgramElement(ProgramElement pe) throws java.io.IOException
pe
- You've guessed it, the ProgramElement to be pretty-printedjava.io.IOException
public void printProgramVariable(ProgramVariable pv) throws java.io.IOException
pv
- The ProgramVariable in the logicjava.io.IOException
public void printProgramSV(ProgramSV pe) throws java.io.IOException
pe
- You've guessed it, the ProgramSV to be pretty-printedjava.io.IOException
protected void printRewrite(Term t) throws java.io.IOException
java.io.IOException
public void printSequent(SequentPrintFilter filter, boolean finalbreak)
public void printSequent(Sequent seq, boolean finalbreak)
public void printSequent(SequentPrintFilter filter)
=>
. 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.filter
- The SequentPrintFilter for seqpublic void printSequent(Sequent seq)
=>
. 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.seq
- The Sequent to be pretty-printedpublic void printSemisequent(Semisequent semiseq) throws java.io.IOException
semiseq
- the semisequent to be printedjava.io.IOException
public void printSemisequent(ImmutableList<SequentPrintFilterEntry> p_formulas) throws java.io.IOException
java.io.IOException
public void printConstrainedFormula(SequentFormula cfma) throws java.io.IOException
cfma
- the constrained formula to be printedjava.io.IOException
public void printTerm(Term t) throws java.io.IOException
t
- the Term to be printedjava.io.IOException
protected ImmutableArray<TermLabel> getVisibleTermLabels(Term t)
Term
. The class SequentViewLogicPrinter
overrides this
method. TermLabel
visibility can be configured via GUI, see
TermLabelMenu
. Default is to print
all TermLabels.public void printLabels(Term t) throws java.io.IOException
java.io.IOException
void printLabels(Term t, java.lang.String left, java.lang.String right) throws java.io.IOException
java.io.IOException
public void printTerm(ImmutableSet<Term> terms) throws java.io.IOException
terms
- the terms to be printedjava.io.IOException
public void printTermContinuingBlock(Term t) throws java.io.IOException
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 & cinstead of
a & b & c
t
- the Term to be printedjava.io.IOException
public void printFunctionTerm(Term t) throws java.io.IOException
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
.t
- the term to be printed.java.io.IOException
public void printCast(java.lang.String pre, java.lang.String post, Term t, int ass) throws java.io.IOException
java.io.IOException
protected boolean printEmbeddedHeapConstructorTerm(Term t) throws java.io.IOException
java.io.IOException
public void printClassName(java.lang.String className) throws java.io.IOException
java.io.IOException
public void printHeapConstructor(Term t, boolean closingBrace) throws java.io.IOException
java.io.IOException
protected void printEmbeddedObserver(Term heapTerm, Term objectTerm) throws java.io.IOException
java.io.IOException
public void printSelect(Term t, Term tacitHeap) throws java.io.IOException
java.io.IOException
public void printStore(Term t, boolean closingBrace) throws java.io.IOException
java.io.IOException
public void printSeqGet(Term t) throws java.io.IOException
java.io.IOException
public void printPostfix(Term t, java.lang.String postfix) throws java.io.IOException
java.io.IOException
public void printObserver(Term t, Term tacitHeap) throws java.io.IOException
java.io.IOException
public void printSingleton(Term t) throws java.io.IOException
java.io.IOException
public void printSeqSingleton(Term t, java.lang.String lDelimiter, java.lang.String rDelimiter) throws java.io.IOException
java.io.IOException
public void printElementOf(Term t) throws java.io.IOException
java.io.IOException
public void printElementOf(Term t, java.lang.String symbol) throws java.io.IOException
java.io.IOException
public void printPrefixTerm(java.lang.String name, Term t, Term sub, int ass) throws java.io.IOException
!a
. No line breaks are possible.name
- the prefix operatort
- whole termsub
- the subterm to be printedass
- the associativity for the subtermjava.io.IOException
public void printPostfixTerm(Term t, int ass, java.lang.String name) throws java.io.IOException
t.a
, where .a
is the postfix operator.
No line breaks are possible.name
- the postfix operatort
- the subterm to be printedass
- the associativity for the subtermjava.io.IOException
public void printInfixTerm(Term l, int assLeft, java.lang.String name, Term t, Term r, int assRight) throws java.io.IOException
p
& q
, where &
is the infix
operator. If line breaks are necessary, the format is like
p & qThe subterms are printed using
printTermContinuingBlock(Term)
.l
- the left subtermassLeft
- associativity for left subtermname
- the infix operatort
- whole termr
- the right subtermassRight
- associativity for right subtermjava.io.IOException
public void printInfixTermContinuingBlock(Term l, int assLeft, java.lang.String name, Term t, Term r, int assRight) throws java.io.IOException
printTermContinuingBlock(Term)
for the
idea. Otherwise like
#printInfixTerm(Term,int,String,Term,int)
.l
- the left subtermassLeft
- associativity for left subtermname
- the infix operatort
- whole termr
- the right subtermassRight
- associativity for right subtermjava.io.IOException
public void printUpdateApplicationTerm(java.lang.String l, java.lang.String r, Term t, int ass3) throws java.io.IOException
{u} t
. If line breaks are necessary, the
format is
{u} t
l
- the left bracer
- the right bracet
- the update termass3
- associativity for phijava.io.IOException
public void printElementaryUpdate(java.lang.String asgn, Term t, int ass2) throws java.io.IOException
loc := val
asgn
- the assignment operator (including spaces)ass2
- associativity for the new valuesjava.io.IOException
private void printParallelUpdateHelper(java.lang.String separator, Term t, int ass) throws java.io.IOException
java.io.IOException
public void printParallelUpdate(java.lang.String separator, Term t, int ass) throws java.io.IOException
java.io.IOException
private void printVariables(ImmutableArray<QuantifiableVariable> vars, LogicPrinter.QuantifiableVariablePrintMode mode) throws java.io.IOException
java.io.IOException
public void printIfThenElseTerm(Term t, java.lang.String keyword) throws java.io.IOException
java.io.IOException
public void printSubstTerm(java.lang.String l, QuantifiableVariable v, Term t, int ass2, java.lang.String r, Term phi, int ass3) throws java.io.IOException
{var/t}s
. If line breaks are necessary, the
format is
{var/t} s
l
- the String used as left brace symbolv
- the QuantifiableVariable
to be substitutedt
- the Term to be used as new valueass2
- the int defining the associativity for the new valuer
- the String used as right brace symbolphi
- the substituted term/formulaass3
- the int defining the associativity for phijava.io.IOException
public void printQuantifierTerm(java.lang.String name, ImmutableArray<QuantifiableVariable> vars, Term phi, int ass) throws java.io.IOException
all x:s.phi
. If line breaks are necessary,
the format is
all x:s. phiNote that the parameter
var
has to contain the
variable name with colon and sort.name
- the name of the quantifiervars
- the quantified variables (+colon and sort)phi
- the quantified formulaass
- associativity for phijava.io.IOException
public void printConstant(java.lang.String s) throws java.io.IOException
s
and
marks it as a nullary term.s
- the constantjava.io.IOException
public void printConstant(Term t, java.lang.String s) throws java.io.IOException
s
and
marks it as a nullary term.t
- constant as term to be printeds
- name of the constantjava.io.IOException
public void printJavaBlock(JavaBlock j) throws java.io.IOException
j
- the Java block to be printedjava.io.IOException
private void printMarkingFirstStatement(java.lang.String s, Range r, Range[] keywords) throws java.io.IOException
r
indicates the `first statement' character range in
string s
. This is sent to the layouter by decomposing
s
into parts and using the appropriate
Layouter.mark(Object)
calls.
This solves the problem that the material in s
might
be further indented.s
- the string containing a programr
- the range of the first statementkeywords
- the ranges of the java keywords in this programjava.io.IOException
private void printVerbatim(java.lang.String s) throws java.io.IOException
Layouter.pre(String)
, but
no block is opened.java.io.IOException
public void printModalityTerm(java.lang.String left, JavaBlock jb, java.lang.String right, Term phi, int ass) throws java.io.IOException
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)
java.io.IOException
public java.lang.String toString()
toString
in class java.lang.Object
public java.lang.StringBuffer result()
protected Layouter mark(LogicPrinter.MarkType type)
protected Layouter mark(LogicPrinter.MarkType type, int parameter)
public PositionTable getPositionTable()
public InitialPositionTable getInitialPositionTable()
public ProgramPrinter programPrinter()
protected Layouter getLayouter()
protected void maybeParens(Term t, int ass) throws java.io.IOException
If prio and associativity are equal, the subterm is printed
using printTermContinuingBlock(Term)
. This currently
only makes a difference for infix operators.
t
- the the subterm to printass
- the associativity for this subtermjava.io.IOException
public SVInstantiations getInstantiations()
protected void markStartSub()
protected void markStartSub(int subterm)
protected void markEndSub()
protected void markStartKeyword()
protected void markStartJavaBlock()
protected void markEndJavaBlock()
protected void markEndKeyword()
protected void startTerm(int size)
size
- the number of rows of the new position tablepublic boolean printInShortForm(java.lang.String attributeProgramName, Term t)
attributeProgramName
- the String of the attribute's program
namet
- the Term used as reference prefixpublic boolean printInShortForm(java.lang.String programName, Sort sort)
programName
- the String denoting the program name of
the attributesort
- the ObjectSort in whose reachable hierarchy
we test for uniquenesspublic static java.lang.String escapeHTML(java.lang.String text, boolean escapeWhitespace)
text
- the String to be displayed as part of an HTML sidepublic static boolean printInShortForm(java.lang.String programName, Sort sort, Services services)
programName
- the String denoting the program name of
the attributesort
- the ObjectSort specifying the hierarchy
where to test for uniquenessservices
- the Services class used to access the type hierarchy