de.uka.ilkd.key.gui.utilities

Class BracketMatchingTextArea.BorderPainter

java.lang.Object

de.uka.ilkd.key.gui.utilities.BracketMatchingTextArea.BorderPainter

All Implemented Interfaces:

javax.swing.text.Highlighter.HighlightPainter

Enclosing class:

BracketMatchingTextArea

private static class BracketMatchingTextArea.BorderPainter
extends java.lang.Object
implements javax.swing.text.Highlighter.HighlightPainter

The Class BorderPainter is a simple highlight painter that just draws a rectangle around the selection.

Field Summary

Fields

Modifier and Type	Field and Description
private java.awt.Color	highlightColor

Constructor Summary

Constructors

Constructor and Description
BorderPainter(java.awt.Color highlightColor)

Method Summary

Modifier and Type	Method and Description
void	paint(java.awt.Graphics g, int offs0, int offs1, java.awt.Shape bounds, javax.swing.text.JTextComponent c) The code is copied from @link DefaultHighlighter#DefaultPainter#paint(Graphics)

Methods inherited from class java.lang.Object

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

Field Detail

highlightColor

private final java.awt.Color highlightColor

Constructor Detail

BorderPainter

public BorderPainter(java.awt.Color highlightColor)

Method Detail

paint

public void paint(java.awt.Graphics g,
                  int offs0,
                  int offs1,
                  java.awt.Shape bounds,
                  javax.swing.text.JTextComponent c)

The code is copied from @link DefaultHighlighter#DefaultPainter#paint(Graphics)

Specified by:

paint in interface javax.swing.text.Highlighter.HighlightPainter