RFR: 8209937: Enhance java.io.Console - provide methods to query console width and height

[Langer, Christoph]

Hi,

please review and give feedback for this augmentation of java.io.Console.

We have users that have the need to query for Width and Height of the console device in Java. In our own JVM implementation we had given them this hook as a custom extension already quite some time ago. We think, however, that it is a worthwhile augmentation of java.io.Console.

Bug: https://bugs.openjdk.java.net/browse/JDK-8209937
Webrev: http://cr.openjdk.java.net/~clanger/webrevs/8209937.0/

I'll also open a CSR for this, but I'll wait for some feedback on our proposal first.

Thanks & Best regards
Christoph