Remove some early code assuming term is an equality type

Move grammar code, mostly simplifying term_grammar

Most significant change sees some code in term_grammar that is only
useful in the concrete syntax parser move to parse_term. Add a _dtype
structure for the latter's public datatypes as well.

correct indent (3 spaces) of documentation in .sig files

first_tok: error message improved; unused code removed

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

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

An alternative fix to r7707: eta expand the declaration of qfail.
This has the advantage of also working in Poly/ML 5.4 Experimental. And, for what it's worth, parse_term can remain polymorphic.

Fixed parse_term.{sig,sml} to remove polymorphism that confused Poly/ML.

It's quite possible that this is a bug in Poly/ML, but it's not as if
we ever used the polymorphism that was present in parse_term before.

Get parse errors from the Absyn stage into exceptions more accurately.

(I noticed that the error message printed out from something like /\ p)
was not the same as the text inside the accompanying HOL_ERR.)

Implement unary minus (the old ~ still also works). Selftest level 2
passes. Changes in the "words world" were replacing $- with -. In
the two quotient changes, I made sure that the infix operator
that used the - character was part of the grammar before it was
parsed. This is necessary because - is now a non-aggregating
character, mainly so that ``--p`` parses as three tokens, not two. Of
course, if you added -- to your grammar, then it would go back to
parsing as two.

Refactor code so that the internal precedence matrix records whether or not
the top thing on the stack is a non-terminal. This should subsequently allow
me to implement unary minus.

Remove more Polyhash occurrences.

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.

Minor bug-fix, which should make the parser behave a little better if
people force it to swallow ambiguous grammars. Also export the
precedence matrix construction function so as to make it a little easier
to see what's really going on interactively.

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.

Relatively radical changes to get rid of the preterm type that lived
in parse_term and replace it with a cleaner Absyn type that Konrad
wrote for TFL.

Slight changes to accomodate parsing into parse_term.preterm ...
which is soon to be changed to "absyn" ...

Two bugs fixed:
1. `foo bar baz)` was parsing OK, because I wasn't requiring that the
lookahead component of the PStack be empty
2. `foo $` and `foo $^t` were both raising Subscript errors; this has
been improved to raise appropriate LEX_ERRORs.

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.

Record field selection implemented as far as parsing and pretty-printing are
concerned.

Implementation of type checking is now entirely above the level of the
kernel. New TCPretype module (type-checking pretype) implements much
of the required functionality, including type unification.
Parse_type generalised to target any type providing the appropriate
constructor functions.

A long-awaited signature file for parse_term.