private void setDefaultHtmlDoctype(String defaultHtmlDoctype) {
    incModificationCount();

    if (Html5SchemaProvider.getHtml5SchemaLocation().equals(defaultHtmlDoctype)) {
      myDefaultHtmlDoctype = HTML5_DOCTYPE_ELEMENT;
    }
    else {
      myDefaultHtmlDoctype = defaultHtmlDoctype;
    }
    fireExternalResourceChanged();
  }
private void setDefaultHtmlDoctype(String defaultHtmlDoctype)