Void setDocumentTitle(HTMLDocument doc, String newtitle)
doc: The HTML document
newtitle: The document title, which may not be blank (an Exception is thrown if it is)
Changes the document title, which is commonly used by browsers when bookmarking the page and in their user interface, and by search engines for indexing purposes. Ideally, all pages should have a unique title.