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 (file)
--- 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)
   {