de.uka.ilkd.key.proof

Class InstantiationProposerCollection

java.lang.Object

de.uka.ilkd.key.proof.InstantiationProposerCollection

All Implemented Interfaces:

InstantiationProposer

public class InstantiationProposerCollection
extends java.lang.Object
implements InstantiationProposer

Composite of instantiation proposers.

Field Summary

Fields

Modifier and Type	Field and Description
private ImmutableList<InstantiationProposer>	proposers

Constructor Summary

Constructors

Constructor and Description
InstantiationProposerCollection()

Method Summary

Modifier and Type	Method and Description
void	add(InstantiationProposer proposer) adds an instantiation proposer to the collection
java.lang.String	getProposal(TacletApp app, SchemaVariable var, Services services, Node undoAnchor, ImmutableList<java.lang.String> previousProposals) Returns an instantiation proposal for the schema variable var.

Methods inherited from class java.lang.Object

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

Field Detail

proposers

private ImmutableList<InstantiationProposer> proposers

Constructor Detail

InstantiationProposerCollection

public InstantiationProposerCollection()

Method Detail

add

public void add(InstantiationProposer proposer)

adds an instantiation proposer to the collection

getProposal

public java.lang.String getProposal(TacletApp app,
                                    SchemaVariable var,
                                    Services services,
                                    Node undoAnchor,
                                    ImmutableList<java.lang.String> previousProposals)

Description copied from interface: InstantiationProposer

Returns an instantiation proposal for the schema variable var.

Specified by:

getProposal in interface InstantiationProposer

Parameters:

app - the taclet app

var - the schema variable to be instantiated

services - pointer to services object

undoAnchor - node to be used as undo anchor

previousProposals - a list of other proposals which should be taken into account (e.g. for name uniqueness), or null