public final void setDocType(DocType docType) {
        if (docType == null) {
            if (_docType != null)
                _children.remove(_docType);
        } else {