trailing newlines in *.{sml,sig} files from src/ removed

Trailing newlines from SML files in src/ were rendered in HTML documentation.

Provide entry point for testing the term lexer.

Parse decimal fractions, turning them into divisions.

Client theories need to overload the magic string

GrammarSpecials.decimal_fraction_special

to their division constant in order to get this to work.

Be smarter about splitting tokens up with whitespace. Now get the
following:
- load "arithmeticTheory";
> val it = () : unit
- ``- -x``;
<<HOL message: inventing new type variable names: 'a>>
> val it = ``--x`` : term
- load "wordsLib";
> val it = () : unit
- ``- -x``;
<<HOL message: inventing new type variable names: 'a>>
> val it = ``- -x`` : term
Would have previously got --x printed in both circumstances, even
though there is a constant -- in wordsTheory.

Handle merging of symbolic characters better when pretty-printing.

Allow differently-based numeric literals. Can now write
0xAF
or
0b1010011
or
063
The latter is octal and requires the flag in base_tokens to be set to
true. (This is a backwards compatibility bodge, just in case there are
people up there who liked leading decimal zeroes.)

Also, all numeric constants can be intermingled with underscores, which
are ignored. These can be used to space numbers for extra legibility.
For example, 12_345_678 is easier to spot as 12 million than 12345678.

Note the convention that numeric type identifier characters don't overlap
with hex digits and are lowercase. For example, 0xAAw would be the word
170. In the potentially ambiguous case of 0xaa, the a is taken to be a
hex digit, not a numeric type specifier.

This commit contains the initial version of the error-location
reporting code I have been working on over the last couple of weeks.

Basically, error messages will now report the source location they
relate to, enabling users to locate bugs more easily within large
definitions.

So far, errors are reported by the lexer, the term parser, and the
datatype parser. Type parser errors will follow, and (hopefully)
typecheck errors.

src/0/locn is a small location-handling library. locn.locn is the
type of locations, and 'a locn.located is a synonym for 'a *
locn.locn. There is a location, Loc_None, for compiler-generated
text, and another, Loc_Unknown, for text of unknown location.

src/0/Feedback now includes some functions for generating located errors.

The lexer now returns located tokens, term_token and type_token
maintain the locations, and parse_term maintains them *internally* on
each terminal and nonterminal. When the system is complete, locations
will persist into absyn and preterm (if I understand the code
correctly!) to enable the typechecker to yield located errors.

I would appreciate any feedback:

* Is the performance impact significant?
* Are any error messages incorrect? (there's a lot of
location-manipulation code in parse_term, some of which I don't
fully understand, and surely some bugs)
* Have I broken anything for anyone, or am I likely to?

The actual output format of the location information is provisional
only, and I intend to generate absolute file positions (rather than
fragment offsets) shortly.

--KW 8-)

NB: tags pre-locn-change and post-locn-change cover this commit.

A complete re-implementation of lexing. Speeds things up considerably
through the use of mosmllex. (The example at the bottom of term_tokens.sml
goes through four to five times faster than it used to.) The basic
design is now more stateful than it used to be. There is a new type,
called the qbuf, which provides buffered access to a quotation. The
implementation of parse_type changes completely because it can no longer
do the monadic-parsing trick of backing up over failed parses. The
implementation of the term parser doesn't really change at all.

Support for new representation of strings.Minor changes.

Changes to bring about Kananaskis parser. Known bug exists in
treatment of qualified identifiers.

Slew of changes to get rid of local open in end in signature files, and
one or two other fixes to make source mosml2.00 compatible. Also added
ability to set and get term_printer function, as per request by Peter
Homeier.

Quite radical changes which allow for "." to be used as the record
field selection operator. Lexer has changed quite dramatically:
it is no longer responsible for determining whether or not a token
is a "keyword" or not. Instead this is done at the parsing level.

The lexer is also now unable to cope with identifiers that are a mix
of alphabetically acceptable and symbolically acceptable characters.

Many changes, mainly to do with record syntax. Also implemented long IDs
as theory-name$id. All of HOL doesn't quite build because field selection
operator is ->, which is used in the real library. Will change this to be
just a simple "." Have also started on concrete syntax for updates.

Numerous changes allowing for printing and parsing of numerals and
treating them as members of different families depending on the contents
of the numeral_info part of the term_grammar. Tested inasmuch the
distribution builds correctly, and with integerTheory loaded.

Fixed to bring it up to date with Taupo release 0.
(Changes have come across from parse_branch development.)