Changes to get Moscow ML impl. to build once more

Includes:
- deletion of unused TermCoding module
- correction of failure to build Holmake
- movement of HOLPP out of impl. specific directories; impl. specific
stuff now in PrettyImpl module

extra semicolons removed from (some) .sig files

Generalise pretty-printers (allowing user implementation thereof).

This is "object oriented" in style: the user can provide an
implementation of the core API to create something of type ppstream.

I think this is necessary to better connect the HOL pretty-printer to the Poly/ML one.

Update PP.with_pp so that it doesn't have to catch Fail exceptions.

Its current behaviour is to catch the exception and print a message
(losing the exception). Now you can avoid the message and get a
message. This is set up as a public boolean ref, and then also made
available as a trace variable.

Update the HOLPP module so that its add_string function uses the
correct size for Unicode characters, and also exports a function
allowing callers to lie about the size of strings being printed.

Move the pretty-printing facilities around a bit so that both SML
implementations use our own version of the PP structure. This
implementation is called HOLPP in src/portableML. After the kernel's
Overlay.sml is loaded, it is also available under the name PP. This
retains fairly good backwards incompatibility. The one deliberate
incompatibility is to make references to General.ppstream invalid.
This makes us better conform with Basis 2002.

The advantage of this manoeuvre is to allow me to better control what
our pretty-printers do at a low level.