de.uka.ilkd.key.pp

Class Notation.Subst

java.lang.Object

de.uka.ilkd.key.pp.Notation

de.uka.ilkd.key.pp.Notation.Subst

Enclosing class:

Notation

public static final class Notation.Subst
extends Notation

The standard concrete syntax for substitution terms.

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

Constructor Summary

Constructors

Constructor and Description
Subst()

Method Summary

Modifier and Type	Method and Description
private QuantifiableVariable	instQV(Term t, LogicPrinter sp, int subTerm)
void	print(Term t, LogicPrinter sp) Print a term to a LogicPrinter.

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

getPriority, printContinuingBlock

Methods inherited from class java.lang.Object

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

Constructor Detail

Subst

public Subst()

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

instQV

private QuantifiableVariable instQV(Term t,
                                    LogicPrinter sp,
                                    int subTerm)