Method saveOptions

basex-core/src/main/java/org/basex/gui/GUI.java:260–270

Saves the current configuration.

()

   * Saves the current configuration.
   */
  public void saveOptions() {
    gopts.setFiles(GUIOptions.OPEN, editor.openFiles());
    final boolean max = getExtendedState() == MAXIMIZED_BOTH;
    gopts.set(GUIOptions.MAXSTATE, max);
    if(!max) {
      gopts.set(GUIOptions.GUILOC, new int[] { getX(), getY()});
      gopts.set(GUIOptions.GUISIZE, new int[] { getWidth(), getHeight()});
    }
    gopts.write();
    context.soptions.write();
  }

  /**
   * Sets the window title.