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.

Fixed config-override of DOT_PATH in Moscow ML

Update mosml smart configuration for mosml 2.10 paths

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.

Fix mosml's basis2002 emulation to include full ListPair module.

This will fix the recent Moscow ML build failures.

Code for the new basis2002 functions is mainly taken from the as-yet
unreleased Moscow ML 2.10, but I have made foldrEq tail-recursive.

Allow Moscow ML build to happen using (as yet unreleased) v2.10.

Basic strategy is to make adoption of basis 2002 even more
thorough. In particular, the Timer structure is now as per
the 2002 Basis.

It is possible to detect that one is working with Moscow ML 2.10 or
later by checking the Holmakefile variable $(HAVE_BASIS2002), which is
set (to value "1") when in 2.10 or later. It is unset elsewhere. See
an example of its use in help/src-sml/Holmakefile.

Recompile mosml basis if Systeml changes.

Also move version detection trick later so that warning message on 2.01
doesn't get in way of reading automatic guesses about config constants.

A nice piece of SML hackery to distinguish Moscow ML versions 2.01 and 2.10.

Reinstate the change from r6056 that made the build work on Windows. I managed to lose this change (to smart-configure.sml) before I moved the contents of that file into configure-mosml.sml.

Now require users to do their configuration from the root HOL
directory (updating the documentation to reflect this). The reason is
to enable both
mosml < tools/smart-configure.sml
and
poly < tools/smart-configure.sml
The contents of tools/smart-configure.sml now figures out which
interpreter is being run (by relying on a known mosml bug), and then
runs the real configuration script for the given ML system.

This would be a lot simpler if mosml's default environment included
the CommandLine structure from the Basis Library.