Added DOCTYPE and Content-type to HTML documents.
authorwebertj
Mon, 30 Jun 2003 12:23:00 +0200
changeset 14083 aed5d25c4a0c
parent 14082 c69d5bf3047d
child 14084 ccb48f3239f7
Added DOCTYPE and Content-type to HTML documents.
src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Sun Jun 29 21:29:15 2003 +0200
+++ b/src/Pure/Thy/html.ML	Mon Jun 30 12:23:00 2003 +0200
@@ -164,8 +164,11 @@
 (* document *)
 
 fun begin_document title =
-  "<html>\n\
+  "<!DOCTYPE HTML PUBLIC \"-//W3C//DTD HTML 4.01 Transitional//EN\" \"http://www.w3.org/TR/html4/loose.dtd\">\n\
+  \\n\
+  \<html>\n\
   \<head>\n\
+  \<meta http-equiv=\"Content-Type\" content=\"text/html; charset=iso-8859-1\">\n\
   \<title>" ^ plain (title ^ " (" ^ version ^ ")") ^ "</title>\n\
   \</head>\n\
   \\n\