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:
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
|
Modifier and Type | Field and Description |
---|---|
private CurrentGoalView |
seqView
the sequentview where dnd has been initiated
|
Constructor and Description |
---|
DragNDropInstantiator(CurrentGoalView seqView) |
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.
|
private CurrentGoalView seqView
DragNDropInstantiator(CurrentGoalView seqView)
public void drop(java.awt.dnd.DropTargetDropEvent event)
public void dragOver(java.awt.dnd.DropTargetDragEvent dtde)
dragOver
in interface java.awt.dnd.DropTargetListener
dragOver
in class java.awt.dnd.DropTargetAdapter
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
java.awt.datatransfer.UnsupportedFlavorException
java.io.IOException
private ImmutableList<PosTacletApp> getAllApplicableApps(PosInSequent sourcePos, PosInSequent targetPos, Services services)
sourcePos
- the PosInSequent where the drag startedtargetPos
- the PosInSequent where the drop occuredservices
- theServices providing access to the program modelprivate ImmutableList<PosTacletApp> getDirectionDependentApps(PosInSequent sourcePos, PosInSequent targetPos, Services services, Sequent sequent)
sourcePos
- PosInSequent where the drag gesture startedtargetPos
- PosInSequent where the drop action took placeservices
- the Servicessequent
- the Sequentprivate ImmutableList<PosTacletApp> getDirectionIndependentApps(PosInSequent sourcePos, PosInSequent targetPos, Services services, Sequent sequent)
sourcePos
- PosInSequent where the drag gesture startedtargetPos
- PosInSequent where the drop action took placeservices
- the Servicessequent
- the Sequentprivate ImmutableList<PosTacletApp> getApplicableTaclets(PosInSequent findPos, DragNDropInstantiator.TacletFilter filter, Services services)
findPos
- the PosInSequent specifying the formula/term that has to be
matched by the find part of a tacletfilter
- the TacletFilter specifying syntactic restrictions on the
taclets to be returnedprivate ImmutableList<PosTacletApp> addPositionInformation(ImmutableList<TacletApp> tacletApps, PosInOccurrence findPos, Services services)
tacletApps
- the IList
with taclet applications to be enriched by
position informationfindPos
- the PosInOccurrence
against which the find part has been
matchedprivate ImmutableList<PosTacletApp> completeIfInstantiations(ImmutableList<PosTacletApp> apps, Sequent seq, PosInOccurrence ifPIO, Services services)
apps
- the IList
with all apps whose if sequent has to
be matched against the formula specified by the pair
seq and ifPIOseq
- the Sequent to which the position information in ifPIO
is relative toifPIO
- the PosInOccurrence describing the position of the term to
be matched against the if sequent of the tacletsservices
- the ServicesIList
that have been matched successfullyprivate ImmutableList<PosTacletApp> completeInstantiations(ImmutableList<PosTacletApp> apps, PosInOccurrence missingSVPIO, Services services)
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 tomissingSVPIO
- the PosInOccurrence describing the position of the term an
uninstantiated SV will be matched againstservices
- the ServicesIList
that have been matched successfullyprivate void execute(PosTacletApp app)
app
- the PosTacletApp to be applied