Make sure all HTML pages are interpreted as utf-8 encoded

E.g. computeLib.CBV_CONV didn't display properly before this commit

Also use the "html5 doctype" in affected files

Ops, links in SVG theory graph must have target="_parent"

Otherwise links are opened inside the object element in the generated HTML page.

Render theory graph as SVG instead of JPEG

Fix DOT script for building theory graph

HOL builds at selftest level 1

Try to find dot in user's PATH during configuration

If it is not found, say little about its absence on help-graph build
time.

Provide slightly better error message when dot doesn't work

Allow user to configure location of dot tool for theory graph building.

The default is /usr/bin/dot, because that’s where it is on my Linux machine. If you need it to be somewhere else, create a config-override or poly-includes.ML file, depending on which ML you’re using.

Pushing things so I can work on case constant flipping.

Theory graph building now quieter, and reports on progress.

Clean up theory-graph production, and DB.print_theory_as_html.

DOT-file generation works in Moscow ML now that we have given Moscow
ML and up-to-date Basis Library. The HTML generation in
print_theory_as_html now attempts to be cleaner, with style-sheets
etc. I'd also like to pass it through to the html_terminal backend
but this causes problems: boolTheory.LCOMM_THM and
relationTheory.TC_DEF both cause the html_terminal/PP combination to
fail.

The theories.html file generated by DOT had a reference to an
absolute filename for the picture. Changed this to be a relative
reference.

Update the theory graph generation code. Omit _emit theories from the
graph. Can be simplified somewhat because dot can now be used to
generate the client map coordinates directly. Don't bother to get it
to work with Moscow ML as well as Poly.

Start working on porting the doc building system to SML (i.e., not Moscow ML)
to get it working with Poly ML.