X-Git-Url: http://source.jalview.org/gitweb/?a=blobdiff_plain;f=src%2Fjalview%2Fgui%2FSplitFrame.java;fp=src%2Fjalview%2Fgui%2FSplitFrame.java;h=3a6d266894ad9cde488804ae7c02b2edc58281aa;hb=5cd32d19826b02d519fd79b7cd26c68bb981c378;hp=9da82401d3a9117cda54a6651741d2f2c77125b8;hpb=cf4a342e06c80456393620b28820fa616fbc221c;p=jalview.git diff --git a/src/jalview/gui/SplitFrame.java b/src/jalview/gui/SplitFrame.java index 9da8240..3a6d266 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; @@ -37,12 +38,15 @@ import java.awt.event.KeyEvent; import java.awt.event.KeyListener; import java.beans.PropertyVetoException; import java.util.Map.Entry; +import java.util.Set; import javax.swing.AbstractAction; import javax.swing.InputMap; import javax.swing.JComponent; import javax.swing.JMenuItem; import javax.swing.KeyStroke; +import javax.swing.UIDefaults; +import javax.swing.UIManager; import javax.swing.event.InternalFrameAdapter; import javax.swing.event.InternalFrameEvent; @@ -81,10 +85,23 @@ 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) + */ + UIDefaults defaults = UIManager.getDefaults(); + Set keySet = defaults.keySet(); + for (Object key : keySet) + { + System.out.println(key.toString() + " = " + + UIManager.get(key).toString()); + } + 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; + + ((AlignFrame) getBottomFrame()).getHeight() + DIVIDER_SIZE + + heightFudge; height = fitHeightToDesktop(height); setSize(width, height);