+
+ af.alignPanel.fontChanged(); // make sure font is updated *before* we set ID width
+ if (view.getIdWidth()==null)
+ {
+ if (!isVersionStringLaterThan("2.11.3", jm.getVersion())) {
+ // Pre 2.11.3 jalview projects do not store the id width
+ // idWidth was also calculated in a different way.
+ viewport.setIdWidth(af.alignPanel.getLegacyIdWidth());
+ af.alignPanel.getIdPanel().getIdCanvas().setManuallyAdjusted(true);
+ }
+ } else {
+ viewport.setIdWidth(view.getIdWidth());
+ af.alignPanel.getIdPanel().getIdCanvas().setManuallyAdjusted(view.isIdWidthManuallyAdjusted());
+ }
+