--- a/src/Pure/Thy/html.scala Wed Feb 13 11:25:23 2019 +0100
+++ b/src/Pure/Thy/html.scala Thu Feb 14 14:44:41 2019 +0100
@@ -324,8 +324,8 @@
/* document */
val header: String =
- """<?xml version="1.0" encoding="utf-8" ?>
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+ XML.header +
+ """<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">"""
val head_meta: XML.Elem =