Fix ParseDatatype bug when parsing Datatype syntax

One test case would be

foo = Con1 bool; bar = Con2 foo (bool -> bool);

which didn't cope with the first semicolon, which is next to the bool
argument without an intervening space.

The previous handling of the "feature" whereby atomic types don't need
to be separated from other arguments involved a recursive call to the
type parser on a specially constructed sub-buffer. This was
disgusting and broken. Now the code just calls a parse_atom function
made visible from inside the type parser.

Add some illustrative test-cases.

Thanks to Oskar Abrahamsson for the bug report.

Improve datatype parsing, including ; as terminator inside records

More tests included.

Allow trailing semicolons in datatype declarations

Also:
- factor out datatype declarations for related AST types so that they
print nicely in Poly/ML interactive loops
- share more code between parsers of old and new syntax

With test-cases.

Closes #446

Fix Datatype parsing array[number] type

Includes test-case

Fix bug identified by test in c2fc2ca

Also fix tests themselves and add another in similar vein.

Fix ParseDatatype to handle recursive redefinitions

Unify handling of type abbrevs and type operators

This is analogous to what is done with terms, where the handling of
genuine constants passes through the overload map.

The main desirable effect should be that if multiple genuine type
operators with the same name are in the grammar, then only one will
print unqualified; all the others will print with theory-qualification.

Currently fails in src/datatype's selftest as ParseDatatype doesn't see
bare names that are existing types as possible occurrences of recursive
types.

Datatype now handles antiquotations.

Closes #258

Implement most of a new Datatype function with nicer syntax.

(Pair-programming with Magnus who wanted it.) Still need to
implement change to EmitTeX.

Fix for an error in datatype declaration parsing when the apostrophe
of a type variable immediately follows the colon in a field type
spec. Originally, found in examples/HolCheck, but have also now moved
an example into the selftest.

Modify lexing so that "mixed" tokens are possible if a user puts them
into the grammar. For example, one might do

set_fixity "-->a" (Infix(NONASSOC, 450))

This then causes ``p -->a q`` to be parsed as an infix application of
-->a to p and q. If you wrote ``p --> a q``, the -->a token would not
be seen. Without -->a being in the grammar, it will be lexed as
before, a symbolic token (-->) followed by an alphanumeric one (a).
(Note also that things like --a--> where the mixing up happens in the
middle of the token, are just as possible.)

This change also allows traditional alphanumeric identifiers to
combine with Unicode subscripts. Using LaTeX notation, a_1 is now
possible.

The system builds with selftest level 1, so I believe I have preserved
backwards compatibility. (I have also added a test to
src/bool/selftest.sml to check for _1 working as a case expression
pattern properly.)

Remove comment full of tests and move them to a selftest file, where they
can be performed automatically.

Adapting to new Basis (and SML/NJ).

Moved from src/datatype.