DocType docType(int line, int col, String elementName,
                  String publicID, String systemID);
DocType docType(int line, int col, String elementName,
                  String publicID, String systemID)