de.uka.ilkd.key.gui.sourceview

Class SourceView.TextPaneMouseAdapter

java.lang.Object

java.awt.event.MouseAdapter

de.uka.ilkd.key.gui.sourceview.SourceView.TextPaneMouseAdapter

All Implemented Interfaces:

java.awt.event.MouseListener, java.awt.event.MouseMotionListener, java.awt.event.MouseWheelListener, java.util.EventListener

Enclosing class:

SourceView

private class SourceView.TextPaneMouseAdapter
extends java.awt.event.MouseAdapter

This listener checks if a highlighted section is clicked. If true, a jump in the proof tree to the most recently created node (in the current branch) containing the highlighted statement is performed.
Note: No jumping down in the proof tree is possible. Implementing this would be non-trivial, because it was not unique into which branch we would want to descent.

Author:

Wolfram Pfeifer

Field Summary

Fields

Modifier and Type	Field and Description
(package private) java.lang.String	filename The filename of the file whose content is displayed in the JTextPane.
(package private) IOUtil.LineInformation[]	li The precalculated start indices of the lines.
(package private) javax.swing.text.Highlighter.HighlightPainter	painter The Painter used for painting the highlights (except for the most recent one).
(package private) javax.swing.JTextPane	textPane The JTextPane containing the source code.

Constructor Summary

Constructors

Constructor and Description
TextPaneMouseAdapter(javax.swing.JTextPane textPane, IOUtil.LineInformation[] li, javax.swing.text.Highlighter.HighlightPainter painter, java.lang.String filename)

Method Summary

Modifier and Type	Method and Description
private boolean	isHighlighted(int pos) Checks if the given position is within a highlight.
void	mouseClicked(java.awt.event.MouseEvent e)

Methods inherited from class java.awt.event.MouseAdapter

mouseDragged, mouseEntered, mouseExited, mouseMoved, mousePressed, mouseReleased, mouseWheelMoved

Methods inherited from class java.lang.Object

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

Field Detail

li

final IOUtil.LineInformation[] li

The precalculated start indices of the lines. Used to compute the clicked line number.

painter

final javax.swing.text.Highlighter.HighlightPainter painter

The Painter used for painting the highlights (except for the most recent one).

textPane

final javax.swing.JTextPane textPane

The JTextPane containing the source code.

filename

final java.lang.String filename

The filename of the file whose content is displayed in the JTextPane.

Constructor Detail

TextPaneMouseAdapter

public TextPaneMouseAdapter(javax.swing.JTextPane textPane,
                            IOUtil.LineInformation[] li,
                            javax.swing.text.Highlighter.HighlightPainter painter,
                            java.lang.String filename)

Method Detail

isHighlighted

private boolean isHighlighted(int pos)

Checks if the given position is within a highlight.

Parameters:

pos - the position to check

Returns:

true if highlighted and false if not

mouseClicked

public void mouseClicked(java.awt.event.MouseEvent e)

Specified by:

mouseClicked in interface java.awt.event.MouseListener

Overrides:

mouseClicked in class java.awt.event.MouseAdapter