MenuElement[] path = new MenuElement[selection.size ()];
MenuElement[] path = new MenuElement[selectedPath.size()];
  public MenuElement[] getSelectedPath ()  {    MenuElement[] path = new MenuElement[selection.size ()];    for (int i = 0; i < path.length; i++)      path[i] = (MenuElement) selection.get (i);    return path;  }