+ if (menu.getId() == 3000) {
+ // Bigger +2
+ assert (getScreen() instanceof SwingTerminal);
+ SwingTerminal terminal = (SwingTerminal) getScreen();
+ terminal.setFontSize(terminal.getFontSize() + 2);
+ return true;
+ }
+ if (menu.getId() == 3001) {
+ // Smaller -2
+ assert (getScreen() instanceof SwingTerminal);
+ SwingTerminal terminal = (SwingTerminal) getScreen();
+ terminal.setFontSize(terminal.getFontSize() - 2);
+ return true;
+ }
+