From: gmungoc Date: Mon, 9 Mar 2020 10:26:59 +0000 (+0000) Subject: JAL-3412 update layout whenever desired id width changes X-Git-Tag: Develop-2_11_2_0-d20201215~79^2~4 X-Git-Url: http://source.jalview.org/gitweb/?a=commitdiff_plain;h=c05539a51cc57a9fabb10e01bb7b2e4123da628c;hp=5442c094270c57798747ee8d974b7ef010f87a82;p=jalview.git JAL-3412 update layout whenever desired id width changes --- diff --git a/src/jalview/gui/AlignmentPanel.java b/src/jalview/gui/AlignmentPanel.java index 85c46bd..dfe0ffa 100644 --- a/src/jalview/gui/AlignmentPanel.java +++ b/src/jalview/gui/AlignmentPanel.java @@ -245,14 +245,17 @@ public class AlignmentPanel extends GAlignmentPanel implements } /** - * Calculate the width of the alignment labels based on the displayed names - * and any bounds on label width set in preferences. + * Calculates the width of the alignment labels based on the displayed names + * and any bounds on label width set in preferences. The calculated width is + * also set as a property of the viewport. * * @return Dimension giving the maximum width of the alignment label panel * that should be used. */ public Dimension calculateIdWidth() { + int oldWidth = av.getIdWidth(); + // calculate sensible default width when no preference is available Dimension r = null; if (av.getIdWidth() < 0) @@ -269,6 +272,16 @@ public class AlignmentPanel extends GAlignmentPanel implements r.width = av.getIdWidth(); r.height = 0; } + + /* + * fudge: if desired width has changed, update layout + * (see also paintComponent - updates layout on a repaint) + */ + if (r.width != oldWidth) + { + idPanelHolder.setPreferredSize(r); + validate(); + } return r; } @@ -820,12 +833,6 @@ public class AlignmentPanel extends GAlignmentPanel implements } } - /** - * DOCUMENT ME! - * - * @param g - * DOCUMENT ME! - */ @Override public void paintComponent(Graphics g) {