DefaultUnderlineHighlightPainter (used for underlines as in find all)
DefaultFrameHighlightPainter (used to draw a box around the highlighted text)
DefaultHighlightPainter (now called only by Swing for a normal highlight)
DrJavaHighlightPainter (a normal highlight requested by DrJava)
The DrJavaHighlightPainter nested class was added in order to differentiate between highlights created by DrJava and those created by Swing (this helps us find the selected text highlight and raise its priority). The insert-in-order operation may cause a slight performance decrease, but is not intended as a long-term solution. Ideally, a better type of storage will be used to make inserting a quicker operation.
M src/edu/rice/cs/drjava/ui/DefinitionsPane.java
M src/edu/rice/cs/drjava/ui/ErrorPanel.java
M src/edu/rice/cs/drjava/ui/AbstractDJPane.java
M src/edu/rice/cs/drjava/ui/ReverseHighlighter.java
M src/edu/rice/cs/util/swing/HighlightManagerTest.java
