v2.16.01: doc: add a few tags to the html output format

It may be possible to generate the printed documentation from the
HTML, with a suitable combination of print-only CSS. Definitely not
there yet, though.