The new HTML output is much better-looking.

Also, switch to use the verbatim environment for code, after much
fighting with LaTeX.  This generates less HTML, and it looks better.