de.uka.ilkd.key.gui.nodeviews

Class DragNDropInstantiator

java.lang.Object

java.awt.dnd.DropTargetAdapter

de.uka.ilkd.key.gui.nodeviews.DragNDropInstantiator

All Implemented Interfaces:

java.awt.dnd.DropTargetListener, java.util.EventListener

public class DragNDropInstantiator
extends java.awt.dnd.DropTargetAdapter

The DragNDropInstantiator interpretes drag'n drop actions as taclet instantiations. The behaviour is described below (excluding some "optimisation" details)

Let "source" denote the formula/term which is dragged and dropped on another term called "target". The DragNDropInstantiation of a taclet "t" is now defined as follows:

1. t must have exactly one formula/term in the find part and assumes sequent (in particular it must have an assumes -part)
2. and
   1. if t's goal descriptions do not contain any replacewith then "source" is matched against the find part of the taclet and "target" has to match the "if" part.
   2. if t's goal descriptions contain at least one replacewith then "target" is matched against the find part and "source" against the assumes part
   or
3. t must have a find part, no assumes and at least one addrule. In this case source is merged against find part and target has to be the complete sequent. Dropping on the sequent arrow is interpreted as applying an addrule(treats hide rules)

The DragNDropInstantiator now determines all taclets, which have a valid drag'n drop instantiation for a given (source, target) position pair. If there is only one taclet with a valid dnd-instantiation this one is executed otherwise the user is presented a list of possible taclets from which she/he can select one.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	DragNDropInstantiator.PopupListener This popup listener listens to the taclet app selection listener and executes the selected app if necessary
protected static interface	DragNDropInstantiator.TacletFilter This interface is impemented by filters selecting certain kinds of taclets depending on their syntactic structure

Field Summary

Fields

Modifier and Type	Field and Description
private CurrentGoalView	seqView the sequentview where dnd has been initiated

Constructor Summary

Constructors

Constructor and Description
DragNDropInstantiator(CurrentGoalView seqView)

Method Summary

Modifier and Type	Method and Description
private ImmutableList<PosTacletApp>	addPositionInformation(ImmutableList<TacletApp> tacletApps, PosInOccurrence findPos, Services services) the taclet applications is given the correct position information where their "find" has been matched
private ImmutableList<PosTacletApp>	completeIfInstantiations(ImmutableList<PosTacletApp> apps, Sequent seq, PosInOccurrence ifPIO, Services services) tries to complete the (partial) taclet instantantiation of the applications given in apps.
private ImmutableList<PosTacletApp>	completeInstantiations(ImmutableList<PosTacletApp> apps, PosInOccurrence missingSVPIO, Services services) tries to complete the (partial) taclet instantantiation of the applications given in apps.
void	dragOver(java.awt.dnd.DropTargetDragEvent dtde)
void	drop(java.awt.dnd.DropTargetDropEvent event)
private void	execute(PosTacletApp app) applies the given app
private ImmutableList<PosTacletApp>	getAllApplicableApps(PosInSequent sourcePos, PosInSequent targetPos, Services services) retrieves all drag'n drop instantiable taclet applications
private ImmutableList<PosTacletApp>	getApplicableTaclets(PosInSequent findPos, DragNDropInstantiator.TacletFilter filter, Services services) retrieves all taclets applicable on the given position and select those that fulfill the given filter condition.
private ImmutableList<PosTacletApp>	getDirectionDependentApps(PosInSequent sourcePos, PosInSequent targetPos, Services services, Sequent sequent) returns all applicable apps respecting direction information in drag an drop
private ImmutableList<PosTacletApp>	getDirectionIndependentApps(PosInSequent sourcePos, PosInSequent targetPos, Services services, Sequent sequent) returns all applicable apps without respecting direction information in drag an drop
private void	interpreteDragAndDropInstantiation(java.awt.dnd.DropTargetDropEvent event, java.awt.Point dropLocation, java.awt.datatransfer.Transferable transferable) Interpretes the drag and drop gesture.

Methods inherited from class java.awt.dnd.DropTargetAdapter

dragEnter, dragExit, dropActionChanged

Methods inherited from class java.lang.Object

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

Field Detail

seqView

private CurrentGoalView seqView

the sequentview where dnd has been initiated

Constructor Detail

DragNDropInstantiator

DragNDropInstantiator(CurrentGoalView seqView)

Method Detail

drop

public void drop(java.awt.dnd.DropTargetDropEvent event)

dragOver

public void dragOver(java.awt.dnd.DropTargetDragEvent dtde)

Specified by:

dragOver in interface java.awt.dnd.DropTargetListener

Overrides:

dragOver in class java.awt.dnd.DropTargetAdapter

interpreteDragAndDropInstantiation

private void interpreteDragAndDropInstantiation(java.awt.dnd.DropTargetDropEvent event,
                                                java.awt.Point dropLocation,
                                                java.awt.datatransfer.Transferable transferable)
                                         throws java.awt.datatransfer.UnsupportedFlavorException,
                                                java.io.IOException

Interpretes the drag and drop gesture. Checks which taclets could be meant by the drag'n drop and applies if the app can be uniquely determined, otherwise a selection menu is presented to the user

Throws:

java.awt.datatransfer.UnsupportedFlavorException

java.io.IOException

getAllApplicableApps

private ImmutableList<PosTacletApp> getAllApplicableApps(PosInSequent sourcePos,
                                                         PosInSequent targetPos,
                                                         Services services)

retrieves all drag'n drop instantiable taclet applications

Parameters:

sourcePos - the PosInSequent where the drag started

targetPos - the PosInSequent where the drop occured

services - theServices providing access to the program model

Returns:

all drag'n drop instantiable taclet applications

getDirectionDependentApps

private ImmutableList<PosTacletApp> getDirectionDependentApps(PosInSequent sourcePos,
                                                              PosInSequent targetPos,
                                                              Services services,
                                                              Sequent sequent)

returns all applicable apps respecting direction information in drag an drop

Parameters:

sourcePos - PosInSequent where the drag gesture started

targetPos - PosInSequent where the drop action took place

services - the Services

sequent - the Sequent

Returns:

all applicable apps respecting direction information in drag an drop

getDirectionIndependentApps

private ImmutableList<PosTacletApp> getDirectionIndependentApps(PosInSequent sourcePos,
                                                                PosInSequent targetPos,
                                                                Services services,
                                                                Sequent sequent)

returns all applicable apps without respecting direction information in drag an drop

Parameters:

sourcePos - PosInSequent where the drag gesture started

targetPos - PosInSequent where the drop action took place

services - the Services

sequent - the Sequent

Returns:

all applicable apps respecting direction information in drag an drop

getApplicableTaclets

private ImmutableList<PosTacletApp> getApplicableTaclets(PosInSequent findPos,
                                                         DragNDropInstantiator.TacletFilter filter,
                                                         Services services)

retrieves all taclets applicable on the given position and select those that fulfill the given filter condition. The filter selects taclets satisfying certain syntactic categories (for example, taclets with at least one replacewith in their goal description or those without any replacewith).

Parameters:

findPos - the PosInSequent specifying the formula/term that has to be matched by the find part of a taclet

filter - the TacletFilter specifying syntactic restrictions on the taclets to be returned

Returns:

the list of taclets which match the term at the given position and satisfy the filter condition

addPositionInformation

private ImmutableList<PosTacletApp> addPositionInformation(ImmutableList<TacletApp> tacletApps,
                                                           PosInOccurrence findPos,
                                                           Services services)

the taclet applications is given the correct position information where their "find" has been matched

Parameters:

tacletApps - the IList with taclet applications to be enriched by position information

findPos - the PosInOccurrence against which the find part has been matched

Returns:

the taclet apps as given in tacletApps but with position information

completeIfInstantiations

private ImmutableList<PosTacletApp> completeIfInstantiations(ImmutableList<PosTacletApp> apps,
                                                             Sequent seq,
                                                             PosInOccurrence ifPIO,
                                                             Services services)

tries to complete the (partial) taclet instantantiation of the applications given in apps. The resulting applications are returned. The given apps must have either all an if part or none of them.

Parameters:

apps - the IList with all apps whose if sequent has to be matched against the formula specified by the pair seq and ifPIO

seq - the Sequent to which the position information in ifPIO is relative to

ifPIO - the PosInOccurrence describing the position of the term to be matched against the if sequent of the taclets

services - the Services

Returns:

the IList that have been matched successfully

completeInstantiations

private ImmutableList<PosTacletApp> completeInstantiations(ImmutableList<PosTacletApp> apps,
                                                           PosInOccurrence missingSVPIO,
                                                           Services services)

tries to complete the (partial) taclet instantantiation of the applications given in apps. The resulting applications are returned.

Parameters:

apps - the IList with all apps whose if sequent has to be matched against the formula specified by the pair seq and ifPIO is relative to

missingSVPIO - the PosInOccurrence describing the position of the term an uninstantiated SV will be matched against

services - the Services

Returns:

the IList that have been matched successfully

execute

private void execute(PosTacletApp app)

applies the given app

Parameters:

app - the PosTacletApp to be applied