public class SequentViewInputListener
extends java.lang.Object
implements java.awt.event.MouseMotionListener, java.awt.event.MouseListener
Modifier and Type | Method and Description |
---|---|
void |
highlightOriginInSourceView(PosInSequent pos)
Highlights the origin of the term at the specified position.
|
static boolean |
isRefresh() |
void |
mouseClicked(java.awt.event.MouseEvent e) |
void |
mouseDragged(java.awt.event.MouseEvent me) |
void |
mouseEntered(java.awt.event.MouseEvent e) |
void |
mouseExited(java.awt.event.MouseEvent e) |
void |
mouseMoved(java.awt.event.MouseEvent me) |
void |
mousePressed(java.awt.event.MouseEvent e) |
void |
mouseReleased(java.awt.event.MouseEvent e) |
static void |
setRefresh(boolean refresh) |
protected void |
showTermInfo(java.awt.Point p)
Show info about the term at the specified point in the status line.
|
public static boolean isRefresh()
public static void setRefresh(boolean refresh)
public void mouseDragged(java.awt.event.MouseEvent me)
mouseDragged
in interface java.awt.event.MouseMotionListener
public void mouseMoved(java.awt.event.MouseEvent me)
mouseMoved
in interface java.awt.event.MouseMotionListener
public void mouseExited(java.awt.event.MouseEvent e)
mouseExited
in interface java.awt.event.MouseListener
public void mouseClicked(java.awt.event.MouseEvent e)
mouseClicked
in interface java.awt.event.MouseListener
public void mousePressed(java.awt.event.MouseEvent e)
mousePressed
in interface java.awt.event.MouseListener
public void mouseReleased(java.awt.event.MouseEvent e)
mouseReleased
in interface java.awt.event.MouseListener
public void mouseEntered(java.awt.event.MouseEvent e)
mouseEntered
in interface java.awt.event.MouseListener
public void highlightOriginInSourceView(PosInSequent pos)
pos
- the position of the term whose origin should be highlighted.protected void showTermInfo(java.awt.Point p)
p
- a point.Copyright © 2003-2019 The KeY-Project.