static KeyListener ctrlEnterKeyListener(fO action) {
  ret new KeyAdapter {
    public void keyReleased(KeyEvent ke) {
      if (ke.getKeyCode() == KeyEvent.VK_ENTER && ke.getModifiers() == KeyEvent.CTRL_MASK)
        pcallF(action);
    }
  };
}