X-Git-Url: http://source.jalview.org/gitweb/?a=blobdiff_plain;f=src%2Fjalview%2Fgui%2FSplitFrame.java;h=083c7ecf135ec2a01be8cb54071b3f1202a0c355;hb=c6c67aaa8e2d236305a3495f4edfc8cc88e22b79;hp=b790d62444114499d84451723f61a007127c4ab2;hpb=db4eacee27b836db4126dca551887bfc6652d72a;p=jalview.git diff --git a/src/jalview/gui/SplitFrame.java b/src/jalview/gui/SplitFrame.java index b790d62..083c7ec 100644 --- a/src/jalview/gui/SplitFrame.java +++ b/src/jalview/gui/SplitFrame.java @@ -26,6 +26,7 @@ import jalview.datamodel.AlignmentI; import jalview.jbgui.GAlignFrame; import jalview.jbgui.GSplitFrame; import jalview.structure.StructureSelectionManager; +import jalview.util.Platform; import jalview.viewmodel.AlignmentViewport; import java.awt.Component; @@ -81,12 +82,17 @@ public class SplitFrame extends GSplitFrame implements SplitContainerI ((AlignFrame) getTopFrame()).getViewport().setCodingComplement( ((AlignFrame) getBottomFrame()).getViewport()); - int width = ((AlignFrame) getTopFrame()).getWidth(); - // about 50 pixels for the SplitFrame's title bar etc + /* + * estimate width and height of SplitFrame; this.getInsets() doesn't seem to + * give the full additional size (a few pixels short) + */ + int widthFudge = Platform.isAMac() ? 28 : 28; // Windows tbc + int heightFudge = Platform.isAMac() ? 50 : 50; // tbc + int width = ((AlignFrame) getTopFrame()).getWidth() + widthFudge; int height = ((AlignFrame) getTopFrame()).getHeight() - + ((AlignFrame) getBottomFrame()).getHeight() + 50; - // about 65 pixels for Desktop decorators on Windows - height = Math.min(height, Desktop.instance.getHeight() - 65); + + ((AlignFrame) getBottomFrame()).getHeight() + DIVIDER_SIZE + + heightFudge; + height = fitHeightToDesktop(height); setSize(width, height); adjustLayout(); @@ -101,6 +107,27 @@ public class SplitFrame extends GSplitFrame implements SplitContainerI } /** + * Reduce the height if too large to fit in the Desktop. Also adjust the + * divider location in proportion. + * + * @param height + * in pixels + * @return original or reduced height + */ + public int fitHeightToDesktop(int height) + { + // allow about 65 pixels for Desktop decorators on Windows + + int newHeight = Math.min(height, Desktop.instance.getHeight() - 65); + if (newHeight != height) + { + int oldDividerLocation = getDividerLocation(); + setDividerLocation(oldDividerLocation * newHeight / height); + } + return newHeight; + } + + /** * Set the top and bottom frames to listen to each others Commands (e.g. Edit, * Order). */