import jalview.renderer.ScaleRenderer.ScaleMark;
import jalview.util.MessageManager;
import jalview.viewmodel.ViewportListenerI;
+import jalview.viewmodel.ViewportRanges;
import java.awt.Color;
import java.awt.FontMetrics;
int res = (evt.getX() / av.getCharWidth())
+ av.getRanges().getStartRes();
- res = av.getAlignment().getHiddenColumns().adjustForHiddenColumns(res);
-
- reveal = null;
- for (int[] region : av.getAlignment().getHiddenColumns()
- .getHiddenRegions())
- {
- if (res + 1 == region[0] || res - 1 == region[1])
- {
- reveal = region;
- break;
- }
- }
+ reveal = av.getAlignment().getHiddenColumns()
+ .getRegionWithEdgeAtRes(res);
repaint();
}
if (av.getShowHiddenMarkers())
{
int widthx = 1 + endx - startx;
- for (int i = 0; i < hidden.getHiddenRegions().size(); i++)
+ List<Integer> positions = hidden.findHiddenRegionPositions();
+ for (int pos : positions)
{
- res = hidden.findHiddenRegionPosition(i) - startx;
+ res = pos - startx;
if (res < 0 || res > widthx)
{
public void propertyChange(PropertyChangeEvent evt)
{
// Respond to viewport change events (e.g. alignment panel was scrolled)
- repaint();
+ // Both scrolling and resizing change viewport ranges: scrolling changes
+ // both start and end points, but resize only changes end values.
+ // Here we only want to fastpaint on a scroll, with resize using a normal
+ // paint, so scroll events are identified as changes to the horizontal or
+ // vertical start value.
+ if (evt.getPropertyName().equals(ViewportRanges.STARTRES))
+ {
+ // scroll event, repaint panel
+ repaint();
+ }
}
}