static void consoleFont(Font font) {
  callOpt(getConsoleTextArea_gen(), "setFont", font);
}