de.uka.ilkd.key.pp

Class Notation.Infix

java.lang.Object

de.uka.ilkd.key.pp.Notation

de.uka.ilkd.key.pp.Notation.Infix

Enclosing class:

Notation

public static final class Notation.Infix
extends Notation

The standard concrete syntax for infix operators.

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.pp.Notation

Notation.CastFunction, Notation.CharLiteral, Notation.Constant, Notation.ElementaryUpdateNotation, Notation.ElementOfNotation, Notation.FunctionNotation, Notation.HeapConstructorNotation, Notation.IfThenElse, Notation.Infix, Notation.LabelNotation, Notation.ModalityNotation, Notation.ModalSVNotation, Notation.NumLiteral, Notation.ObserverNotation, Notation.ParallelUpdateNotation, Notation.Postfix, Notation.Prefix, Notation.Quantifier, Notation.SchemaVariableNotation, Notation.SelectNotation, Notation.SeqConcatNotation, Notation.SeqGetNotation, Notation.SeqSingletonNotation, Notation.SingletonNotation, Notation.StoreNotation, Notation.Subst, Notation.UpdateApplicationNotation, Notation.VariableNotation

Field Summary

Fields

Modifier and Type	Field and Description
private int	assLeft
private int	assRight
private java.lang.String	name

Constructor Summary

Constructors

Constructor and Description
Infix(java.lang.String name, int prio, int assLeft, int assRight)

Method Summary

Modifier and Type	Method and Description
void	print(Term t, LogicPrinter sp) Print a term to a LogicPrinter.
void	printContinuingBlock(Term t, LogicPrinter sp) Print a term without beginning a new block.

Methods inherited from class de.uka.ilkd.key.pp.Notation

getPriority

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

name

private final java.lang.String name

assLeft

private final int assLeft

assRight

private final int assRight

Constructor Detail

Infix

public Infix(java.lang.String name,
             int prio,
             int assLeft,
             int assRight)

Method Detail

print

public void print(Term t,
                  LogicPrinter sp)
           throws java.io.IOException

Description copied from class: Notation

Print a term to a LogicPrinter. Concrete subclasses override this to call one of the printXYZTerm of LogicPrinter, which do the layout.

Specified by:

print in class Notation

Throws:

java.io.IOException

printContinuingBlock

public void printContinuingBlock(Term t,
                                 LogicPrinter sp)
                          throws java.io.IOException

Print a term without beginning a new block. This calls the LogicPrinter.printTermContinuingBlock(Term) method.

Overrides:

printContinuingBlock in class Notation

Throws:

java.io.IOException