de.uka.ilkd.key.pp

Class IdentitySequentPrintFilter

java.lang.Object

de.uka.ilkd.key.pp.SequentPrintFilter

de.uka.ilkd.key.pp.IdentitySequentPrintFilter

public class IdentitySequentPrintFilter
extends SequentPrintFilter

Identity Filter not doing anything

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	IdentitySequentPrintFilter.IdentityFilterEntry A filter entry, representing one sequent formula.

Field Summary

Fields inherited from class de.uka.ilkd.key.pp.SequentPrintFilter

antec, originalSequent, succ

Constructor Summary

Constructors

Constructor and Description
IdentitySequentPrintFilter()

Method Summary

Modifier and Type	Method and Description
protected SequentPrintFilterEntry	filterFormula(SequentFormula sequentFormula)
protected void	filterSequent() filters the sequent, creating SequentPrintFilterEntries from the sequent formulae.
ImmutableList<SequentPrintFilterEntry>	getFilteredAntec() Get the formulas of the filtered antecedent and the constraints to use for instantiating metavariables when printing
ImmutableList<SequentPrintFilterEntry>	getFilteredSucc() Get the formulas of the filtered succcedent and the constraints to use for instantiating metavariables when printing

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

filterIdentity, getOriginalSequent, setSequent

Methods inherited from class java.lang.Object

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

Constructor Detail

IdentitySequentPrintFilter

public IdentitySequentPrintFilter()

Method Detail

filterSequent

protected void filterSequent()

filters the sequent, creating SequentPrintFilterEntries from the sequent formulae.

Specified by:

filterSequent in class SequentPrintFilter

filterFormula

protected SequentPrintFilterEntry filterFormula(SequentFormula sequentFormula)

Parameters:

sequentFormula - the formula to filter

Returns:

the FilterEntry from the formula

getFilteredAntec

public ImmutableList<SequentPrintFilterEntry> getFilteredAntec()

Get the formulas of the filtered antecedent and the constraints to use for instantiating metavariables when printing

Overrides:

getFilteredAntec in class SequentPrintFilter

Returns:

the filtered antecedent

getFilteredSucc

public ImmutableList<SequentPrintFilterEntry> getFilteredSucc()

Get the formulas of the filtered succcedent and the constraints to use for instantiating metavariables when printing

Overrides:

getFilteredSucc in class SequentPrintFilter

Returns:

the filtered succcedent