class CurrentGoalViewListener
extends java.lang.Object
implements java.awt.event.MouseListener, java.awt.dnd.DragGestureListener
Modifier and Type | Field and Description |
---|---|
private long |
block
hack to block a click event
|
private CurrentGoalView |
currentGoalView |
private KeYMediator |
mediator |
private TacletMenu |
menu |
private boolean |
modalDragNDropEnabled |
private static int |
POPUP_DELAY |
Constructor and Description |
---|
CurrentGoalViewListener(CurrentGoalView currentGoalView,
KeYMediator mediator) |
Modifier and Type | Method and Description |
---|---|
void |
dragGestureRecognized(java.awt.dnd.DragGestureEvent dgEvent)
a drag gesture has been initiated
|
void |
hideMenu() |
boolean |
modalDragNDropEnabled() |
void |
mouseClicked(java.awt.event.MouseEvent me) |
void |
mouseEntered(java.awt.event.MouseEvent me) |
void |
mouseExited(java.awt.event.MouseEvent me) |
void |
mousePressed(java.awt.event.MouseEvent me) |
void |
mouseReleased(java.awt.event.MouseEvent me) |
void |
setModalDragNDropEnabled(boolean allowDragNDrop) |
private static final int POPUP_DELAY
private final KeYMediator mediator
private final CurrentGoalView currentGoalView
private TacletMenu menu
private boolean modalDragNDropEnabled
private long block
CurrentGoalViewListener(CurrentGoalView currentGoalView, KeYMediator mediator)
public void mouseExited(java.awt.event.MouseEvent me)
mouseExited
in interface java.awt.event.MouseListener
public void mouseClicked(java.awt.event.MouseEvent me)
mouseClicked
in interface java.awt.event.MouseListener
public void mousePressed(java.awt.event.MouseEvent me)
mousePressed
in interface java.awt.event.MouseListener
public void mouseReleased(java.awt.event.MouseEvent me)
mouseReleased
in interface java.awt.event.MouseListener
public void mouseEntered(java.awt.event.MouseEvent me)
mouseEntered
in interface java.awt.event.MouseListener
public void hideMenu()
public final void setModalDragNDropEnabled(boolean allowDragNDrop)
public boolean modalDragNDropEnabled()
public void dragGestureRecognized(java.awt.dnd.DragGestureEvent dgEvent)
dragGestureRecognized
in interface java.awt.dnd.DragGestureListener