de.uka.ilkd.key.control

Interface RuleCompletionHandler

All Known Implementing Classes:

AbstractMediatorUserInterfaceControl, ConsoleUserInterfaceControl, WindowUserInterfaceControl

public interface RuleCompletionHandler

Instances of this class are used by an AbstractProofControl to complete a Rule completion.

Author:

Martin Hentschel

Method Summary

Modifier and Type	Method and Description
void	completeAndApplyTacletMatch(TacletInstantiationModel[] models, Goal goal) called to complete and apply a taclet instantiations
IBuiltInRuleApp	completeBuiltInRuleApp(IBuiltInRuleApp app, Goal goal, boolean forced) completes rule applications of built in rules

Method Detail

completeAndApplyTacletMatch

void completeAndApplyTacletMatch(TacletInstantiationModel[] models,
                                 Goal goal)

called to complete and apply a taclet instantiations

Parameters:

models - the partial models with all different possible instantiations found automatically

goal - the Goal where to apply

completeBuiltInRuleApp

IBuiltInRuleApp completeBuiltInRuleApp(IBuiltInRuleApp app,
                                       Goal goal,
                                       boolean forced)

completes rule applications of built in rules

Parameters:

app - the DefaultBuiltInRuleApp to be completed

goal - the Goal where the app will later be applied to

forced - a boolean indicating if the rule should be applied without any additional interaction from the user provided that the application object can be made complete automatically

Returns:

a complete app or null if no completion was possible