+ // 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))
+ {
+ fastPaint((int) evt.getNewValue() - (int) evt.getOldValue());
+ }
+ else if (evt.getPropertyName().equals(ViewportRanges.STARTRESANDSEQ))
+ {
+ fastPaint(((int[]) evt.getNewValue())[0]
+ - ((int[]) evt.getOldValue())[0]);
+ }
+ else if (evt.getPropertyName().equals(ViewportRanges.MOVE_VIEWPORT))
+ {
+ repaint();
+ }
+ }
+
+ /**
+ * computes the visible height of the annotation panel
+ *
+ * @param adjustPanelHeight
+ * - when false, just adjust existing height according to other
+ * windows
+ * @param annotationHeight
+ * @return height to use for the ScrollerPreferredVisibleSize
+ */
+ public int adjustForAlignFrame(boolean adjustPanelHeight,
+ int annotationHeight)
+ {
+ /*
+ * Estimate available height in the AlignFrame for alignment +
+ * annotations. Deduct an estimate for title bar, menu bar, scale panel,
+ * hscroll, status bar, insets.
+ */
+ int stuff = (ap.getViewName() != null ? 30 : 0)
+ + (Platform.isAMac() ? 120 : 140);
+ int availableHeight = ap.alignFrame.getHeight() - stuff;
+ int rowHeight = av.getCharHeight();
+
+ if (adjustPanelHeight)