X-Git-Url: http://git.nikiroo.be/?a=blobdiff_plain;f=src%2Fjexer%2Ftterminal%2FECMA48.java;h=c277795d69450b2db44f79d77a1caa8062c11275;hb=955c55b766a8aebb528d5af5f7582a857c72e2f5;hp=93ae3cd91930ca2f12bea2c38024b2c3408a0b33;hpb=070fba619e47056c00e53bdb4c7684c38e47dca6;p=fanfix.git diff --git a/src/jexer/tterminal/ECMA48.java b/src/jexer/tterminal/ECMA48.java index 93ae3cd..c277795 100644 --- a/src/jexer/tterminal/ECMA48.java +++ b/src/jexer/tterminal/ECMA48.java @@ -871,10 +871,10 @@ public class ECMA48 implements Runnable { case XTERM: // "I am a VT220" - 7 bit version if (!s8c1t) { - return "\033[?62;1;6c"; + return "\033[?62;1;6;9;4c"; } // "I am a VT220" - 8 bit version - return "\u009b?62;1;6c"; + return "\u009b?62;1;6;9;4c"; default: throw new IllegalArgumentException("Invalid device type: " + type); } @@ -1092,7 +1092,7 @@ public class ECMA48 implements Runnable { * * @param width the new width */ - public final void setWidth(final int width) { + public final synchronized void setWidth(final int width) { this.width = width; rightMargin = width - 1; if (currentState.cursorX >= width) { @@ -1117,7 +1117,7 @@ public class ECMA48 implements Runnable { * * @param height the new height */ - public final void setHeight(final int height) { + public final synchronized void setHeight(final int height) { int delta = height - this.height; this.height = height; scrollRegionBottom += delta; @@ -4721,10 +4721,26 @@ public class ECMA48 implements Runnable { int i = getCsiParam(0, 0); if (!xtermPrivateModeFlag) { - if (i == 14) { - // Report xterm window in pixels as CSI 4 ; height ; width t + switch (i) { + case 14: + // Report xterm text area size in pixels as CSI 4 ; height ; + // width t writeRemote(String.format("\033[4;%d;%dt", textHeight * height, textWidth * width)); + break; + case 16: + // Report character size in pixels as CSI 6 ; height ; width + // t + writeRemote(String.format("\033[6;%d;%dt", textHeight, + textWidth)); + break; + case 18: + // Report the text are size in characters as CSI 8 ; height ; + // width t + writeRemote(String.format("\033[8;%d;%dt", height, width)); + break; + default: + break; } } }