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 |
---|---|
protected static interface |
DragNDropInstantiator.TacletFilter
This interface is impemented by filters selecting certain kinds of
taclets depending on their syntactic structure
|
Modifier and Type | Method and Description |
---|---|
void |
dragOver(java.awt.dnd.DropTargetDragEvent dtde) |
void |
drop(java.awt.dnd.DropTargetDropEvent event) |
Copyright © 2003-2019 The KeY-Project.