import java.awt.event.MouseListener;
import java.awt.event.MouseMotionListener;
import java.beans.PropertyChangeEvent;
+import java.util.Iterator;
import java.util.List;
import javax.swing.JMenuItem;
{
av.showColumn(reveal[0]);
reveal = null;
- ap.paintAlignment(true);
+ ap.paintAlignment(true, true);
av.sendSelection();
}
});
{
av.showAllHiddenColumns();
reveal = null;
- ap.paintAlignment(true);
+ ap.paintAlignment(true, true);
av.sendSelection();
}
});
av.setSelectionGroup(null);
}
- ap.paintAlignment(true);
+ ap.paintAlignment(true, true);
av.sendSelection();
}
});
sg.setEndRes(max);
}
av.setSelectionGroup(sg);
- ap.paintAlignment(false);
+ ap.paintAlignment(false, false);
av.sendSelection();
}
}
else
{
- ap.paintAlignment(false);
+ ap.paintAlignment(false, false);
}
return;
}
}
}
stretchingGroup = false;
- ap.paintAlignment(false);
+ ap.paintAlignment(false, false);
av.sendSelection();
}
{
stretchingGroup = true;
cs.stretchGroup(res, sg, min, max);
- ap.paintAlignment(false);
+ ap.paintAlignment(false, false);
}
}
if (av.getShowHiddenMarkers())
{
- List<Integer> positions = hidden.findHiddenRegionPositions(startx,
+ Iterator<Integer> it = hidden.getBoundedStartIterator(startx,
startx + widthx + 1);
- for (int pos : positions)
+ while (it.hasNext())
{
- res = pos - startx;
+ res = it.next() - startx;
gg.fillPolygon(
new int[]
- { -1 + res * avCharWidth - avCharHeight / 4,
- -1 + res * avCharWidth + avCharHeight / 4,
- -1 + res * avCharWidth },
- new int[]
- { y, y, y + 2 * yOf }, 3);
+ { -1 + res * avCharWidth - avCharHeight / 4,
+ -1 + res * avCharWidth + avCharHeight / 4,
+ -1 + res * avCharWidth }, new int[]
+ { y, y, y + 2 * yOf }, 3);
}
}
}
// 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))
+ if (evt.getPropertyName().equals(ViewportRanges.STARTRES)
+ || evt.getPropertyName().equals(ViewportRanges.STARTRESANDSEQ)
+ || evt.getPropertyName().equals(ViewportRanges.MOVE_VIEWPORT))
{
// scroll event, repaint panel
repaint();