WIP for change to list syntax handling.

Very broken at the moment

Remove complicated behaviour behind Unicode trace/flag

Now the Unicode trace is just an inverted handle on the behaviour behind
the PP.avoid_unicode trace. I couldn't use the alias machinery for
this because of the inversion, but they can still alias to the same
underlying SML reference.

While the ProvideUnicode structure still exists it is dramatically
simpler (I decided I didn't want to cut and paste it into the already-
quite-long-enough Parse.sml).

Closes #363

Fix unicode_version to record grammar-deltas

This should ensure that exported grammars pick up all unicode-related
deltas.

The API in ProvideUnicode has changed a bit, but I don't care because
the whole module is going to die in the short-to-medium term anyway.

Remove some unused code in ProvideUnicode.sml

Clean up ProvideUnicode to use proper term-coding

Exploiting the change in 6b52435

ProvideUnicode is probably for the chop anyway (see github issue #363),
but this makes it work a bit more cleanly than it used to.

Record overload_on calls in GrammarDeltas

Give Theory Data writers access to term-writing

Just as readers get an additional parameter of type string -> term,
writers will get a parameter of type term -> string.

Make theory data types provide terms function

This function takes a value of the theory-data type and returns a list
of terms that are contained inside this value. The machinery will use
that to prime the theory's sharing tables to allow for efficient
recording of terms in data.

Give ThyData access to a term-reader function

No useful way to exploit this just yet, but the code compiles and I
think the refactoring is right.

Remove BRULE constructor from user_delta type

It is redundant, though the GRULE representation of a grammar's binder
rule contains information that is never used.

Properly re-org grammar code, removing rule_fixity

Now there is just one fixity type. Also decide that set_fixity and
set_mapped_fixity shouldn't be in the grammar-delta type; instead the
"remove-termtok" and "add_rule" actions (which can be used to implement
the above) should be.

Refactor more grammar code

Ultimate is to switch to concrete "grammar-deltas" in theory files
rather than calls to the update_grms function. Start this process by
extending existing delta type with SET_MAPPED_FIXITY constructor. This
is not yet used.

Rename TruePrefix to Prefix; use fixity options with NONE for what was Prefix.

90+% of this work was done by Ramana Kumar. The following list are
the commits for a series of individual commits that have been squished
into one big change:
* remove mention of TruePrefix from the add_rule docfile
* first batch of changes removing TruePrefix from src/parse
* replace TruePrefix by Prefix in boolScript.sml
* remove TruePrefix from Rsyntax
is a fixity ever required for new_specification?
* some more Prefix -> NONE and TruePrefix -> Prefix in theories
* TruePrefix changes for datatype
* TruePrefix changes for res_quan
* TruePrefix->Prefix in a TeX selftest
* TruePrefix changes for quotient
* TruePrefix changes for integer and real
* fix quotient examples for TruePrefix removal
* more fixes for quotient examples
* fixes for lambda example for TruePrefix removal
* Reword description manual in light of removal of TruePrefix.
* Fix msgTheory quotient example; Poly 5.3 had problems with monotypes.
* Fixes for files in examples/lambda given removal of TruePrefix.
* Fix in examples/unification given removal of TruePrefix.
* Fix in examples/HolCheck given removal of TruePrefix.
* Fixes in examples/acl2 given removal of TruePrefix.

Fix another Unicode-bounce bug.

The real problem in the previous bug was that the Unicode flag was being
bounced as a term was printed for inclusion in the generated theory file.
The previous fix merely removed the bouncing. This fix deals with the
code around the bouncing properly, and simplifies the handling of Unicode
overloads.

Rework grammar infrastructure, losing 'preference' for concrete syntax.

Instead, the most recent rule is the one the pretty-printer will prefer.
The clear_prefs function disappears, but the prefer_form function stays
because it can just adjust the timestamp on the desired form to be most
recent.

Fix pprint bug with Unicode binders in ProvideUnicode and add selftest.

Backout part of previous change, which twigged a Poly/ML bug.

More serious redesign of parser persistence still required.

Get ProvideUnicode to compile under Moscow ML.

Add debugging entrypoint to ProvideUnicode module.

Bugfix: unsetting Unicode trace wasn't correctly removing all Unicode rules.

Reworked implementation of Unicode structure.

Unicode is now a sub-structure of Parse, with functionality provided
by a separate ProvideUnicode module. This organisation makes Parse
the primary module once again (previously Unicode built on top of
Parse).

Changes in src/bool result from

open Parse Unicode

not working. Instead the two opens must be in separate lines:

open Parse
open Unicode