From c05539a51cc57a9fabb10e01bb7b2e4123da628c Mon Sep 17 00:00:00 2001 From: gmungoc Date: Mon, 9 Mar 2020 10:26:59 +0000 Subject: [PATCH] JAL-3412 update layout whenever desired id width changes --- src/jalview/gui/AlignmentPanel.java | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) 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) { -- 1.7.10.2