+ if ((displayListener != null)
+ && (type == DeviceType.XTERM)
+ ) {
+ // For xterms, reset to the actual width, not 80
+ // columns.
+ width = displayListener.getDisplayWidth();
+ rightMargin = width - 1;
+ } else {
+ rightMargin = 79;
+ width = rightMargin + 1;
+ }