More utility entry-points in modules to do with Unicode and UTF8

Provide a Unicode ++ symbol for APPEND

Happy to revert this if people hate the look of it - this is mostly an
experiment.

Provide support for Unicode subscript 'r'

Thinking that this might be a reasonable annotation for relationScript's
set operators. For example, R1 RUNION R2 might be written R1 ∪ᵣ R2

extra semicolons removed from (some) .sig files

Add UnicodeChars entries for quotation marks.

These correspond to the HTML entities &{l,r}{s,d}quo; hence the names
chosen.

Add some nice Unicode brackets to our list of useful characters.

Clean up UnicodeChars implementation.

In particular:
* Use U function everywhere so that Unicode code-points are more
obvious. Instead of "\u00e2\u0088\u0080", U 0x2200 is much more
obviously a reference to U+2200 (forall). This also allows us to
switch away from the UTF-8 encoding more easily if necessary.
* Include more Greek letters.

Fix handling of special 'U' constant, retaining better backwards compatibility.

In particular, there is now a special form 'univ' that behaves as 'U' did.
Further, with Unicode on, the character U+1D54C is used in the same way.
This character may not be in many fonts, so add another trace to turn its
use off. If you can see it, it's a nice 'double-struck' U. I would have
gone for a script-style U, but it leant over too much, and so overlapped
the following left-paren character.

Fix value of UnicodeChars.sup_1 and add more superscript bindings.

some more unicode characters added, mainly arrows and stars

Modify the lexer to handle Unicode tokens properly. For example, you
can type the equivalent of \forall\tau_1 and it will split this blob
of three Unicode characters (and some larger number of bytes) into two
tokens (\forall followed by \tau_1). The pretty-printer also knows
about token categories.

Fairly dramatic change, supporting the use of "syntactic patterns".
It is now possible to overload a name to term (typically a
lambda-abstraction) in order to create syntax-only definitions. For
example, there is a definition of not-equals now in the system:
val _ = overload_on ("<>", ``\x y. ~(x = y)``)
val _ = set_fixity "<>" (Infix(NONASSOC, 450))
This definition is parsed and pretty-printed.

Two other annoying changes. The interface for adding unicode variants
has changed, and I have made precedence level 450 of the parser
non-associative. This latter change has caused most of the (minor)
adjustments to the files below. The regression test doesn't go
through yet. (Currently there is a failure in
quotient/examples/sigma that I don't understand.)

Add some more Unicode characters to the "standard list" in
UnicodeChars. In particular, add superscript minus, and superscript
1, thinking of setting up a concatenation of the two as an inversion
suffix operator at some later date.

More time-wasting, err, addition of arrow characters to UnicodeChars.

Add some symbols for the numeric types.

Use superscript plus to make transitive closure look nice in "Unicode mode".

Add some simplistic code for decoding and encoding UTF8 strings. Also
add even more naive "character" categorisation functions to
UnicodeChars.

Move the structure defining the "useful" Unicode characters into
portableML, but keep Unicode.UChar as a reference to the same
information. (Gotta love the SML module system.)