Method setDisplayFormat

src/tree/TreeRule.java:722–727

@param display_format Optional format string to alter the display name

(String display_format)

  /** @param display_format Optional format string to alter the display name */
  public void setDisplayFormat(String display_format) {
    if (!this.display_format.equals(display_format)) {
      changed.put("display_format", true);
      this.display_format = display_format;
    }
  }

  /** @param level The top level processing order. Must be 0 or greater 
   * @throws IllegalArgumentException if the level was negative */