static KeyStroke ctrlKeyStroke(int keyCode) {
  ret KeyStroke.getKeyStroke(keyCode, InputEvent.CTRL_MASK);
}