/**
* Text window width getter
+ *
+ * @return the window width
*/
public int getWindowWidth() {
return windowWidth;
/**
* Text window height getter
+ *
+ * @return the window height
*/
public int getWindowHeight() {
return windowHeight;
}
+
+ /**
+ * Re-query the text window size
+ */
+ public void queryWindowSize() {
+ // NOP
+ }
+
}