/*
- * Jalview - A Sequence Alignment Editor and Viewer ($$Version-Rel$$)
- * Copyright (C) $$Year-Rel$$ The Jalview Authors
+ * Jalview - A Sequence Alignment Editor and Viewer (Version 2.9.0b1)
+ * Copyright (C) 2015 The Jalview Authors
*
* This file is part of Jalview.
*
import jalview.jbgui.GAlignFrame;
import jalview.jbgui.GSplitFrame;
import jalview.structure.StructureSelectionManager;
+import jalview.util.Platform;
import jalview.viewmodel.AlignmentViewport;
import java.awt.Component;
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;
((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<Object> 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;
- // 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();
}
/**
+ * 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).
*/