Render non-ASCII characters using numeric character references, to simplify
charset issues.  There's a META tag saying the charset is UTF-8, but GHC
outputs characters as raw bytes.

Ideally we need an encoding on the input side too, primarily in comments,
because source files containing non-ASCII characters aren't portable between
locales.