src/Pure/Thy/html.ML
changeset 27896 220e7a18a8ea
parent 27861 911bf8e58c4c
child 28840 049f0a8faa35
equal deleted inserted replaced
27895:e4f8763b971b 27896:220e7a18a8ea
   272 fun with_charset s = setmp_noncritical charset s;
   272 fun with_charset s = setmp_noncritical charset s;
   273 
   273 
   274 fun begin_document title =
   274 fun begin_document title =
   275   let val cs = ! charset in
   275   let val cs = ! charset in
   276     "<?xml version=\"1.0\" encoding=\"" ^ cs ^ "\" ?>\n\
   276     "<?xml version=\"1.0\" encoding=\"" ^ cs ^ "\" ?>\n\
   277     \<!DOCTYPE HTML PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \
   277     \<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \
   278     \\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n\
   278     \\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n\
   279     \<html xmlns=\"http://www.w3.org/1999/xhtml\">\n\
   279     \<html xmlns=\"http://www.w3.org/1999/xhtml\">\n\
   280     \<head>\n\
   280     \<head>\n\
   281     \<meta http-equiv=\"Content-Type\" content=\"text/html; charset=" ^ cs ^ "\"/>\n\
   281     \<meta http-equiv=\"Content-Type\" content=\"text/html; charset=" ^ cs ^ "\"/>\n\
   282     \<title>" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\
   282     \<title>" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\