Method set

basex-core/src/main/java/org/basex/gui/GUI.java:542–548

Sets an option if its value differs from current value and displays the command in the info view. @param option type @param value type @param opt option to be set @param val value

(final T opt, final V val)

   * @param val value
   */
  public <T extends Option<V>, V> void set(final T opt, final V val) {
    if(!context.options.get(opt).toString().equals(val.toString())) {
      final Set cmd = new Set(opt, val);
      cmd.run(context);
      info.setInfo(cmd.info(), cmd, true, false);
    }
  }

  /**
   * Sets the border of the content area.