+ public void setWidth(int newWidth)
+ {
+ if (newWidth < MIN_ID_WIDTH)
+ {
+ return;
+ }
+ final AlignViewportI viewport = ap.getAlignViewport();
+ viewport.setIdWidth(newWidth);
+ ap.paintAlignment(true, false);
+ }
+
+ public boolean manuallyAdjusted()
+ {
+ return manuallyAdjusted;
+ }
+
+ @Override