de.uka.ilkd.key.gui

Class LoopApplyHeadCompletion

java.lang.Object

de.uka.ilkd.key.gui.LoopApplyHeadCompletion

All Implemented Interfaces:

InteractiveRuleApplicationCompletion

public class LoopApplyHeadCompletion
extends java.lang.Object
implements InteractiveRuleApplicationCompletion

Interactive completion for LoopApplyHeadBuiltInRuleApp.

Constructor Summary

Constructors

Constructor and Description
LoopApplyHeadCompletion(MainWindow mainWindow)

Method Summary

Modifier and Type	Method and Description
boolean	canComplete(IBuiltInRuleApp app) checks if this instance is responsible for the given app
IBuiltInRuleApp	complete(IBuiltInRuleApp application, Goal goal, boolean force) method called to complete the given builtin rule application

Methods inherited from class java.lang.Object

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

Constructor Detail

LoopApplyHeadCompletion

LoopApplyHeadCompletion(MainWindow mainWindow)

Method Detail

complete

public IBuiltInRuleApp complete(IBuiltInRuleApp application,
                                Goal goal,
                                boolean force)

Description copied from interface: InteractiveRuleApplicationCompletion

method called to complete the given builtin rule application

Specified by:

complete in interface InteractiveRuleApplicationCompletion

Parameters:

application - the app to complete

goal - the goal where the app will be applied

force - a boolean indicating if the user shall be bothered if the instantiation is unique or can be chosen in a reasonable way as if unique

Returns:

the completed app or null if completion was not possible

canComplete

public boolean canComplete(IBuiltInRuleApp app)

Description copied from interface: InteractiveRuleApplicationCompletion

checks if this instance is responsible for the given app

Specified by:

canComplete in interface InteractiveRuleApplicationCompletion

Parameters:

app - the rule app

Returns:

true iff this instance might be able to complete the app