Move p/printing of set comprehensions out of src/parse

The code for this can be put into pred_set/src/pred_setpp, making the
core pretty-printer slightly simpler (which has to be a good thing).

Also fix the minor pretty-printing indentation bug identified in
github issue #610.

Making this a "user pretty printer" means that it takes precedence
over overloads. Introduce a new feature whereby adding a
(dummy) user-printer with the empty name causes terms matching this
pattern to be printed without any user-printers getting a chance to
fire. This gives terms that are handled by overloads a chance to be
seen by the core printing machinery. (User printers are checked for
first and can otherwise mask everything else.)

Closes #610

Restore ppstream_funs as nullary type operator in term_pp_types

This name is used in user-written code (users' special purpose
pretty-printers), and there is no reason to rebind this name, forcing
them to change things.

Move smpp to Portable - get everything up to arithmeticScript working

Work towards use of PolyML.pretty type for most pretty-printing

Compiles up to src/parse under Poly/ML

User pp fns can note terms as binders to system printer

This allows better behaviour in a test case shown to me by Mike, where
annotations in monad-syntax weren't appearing.

Allow pretty-printing backends to modify grammar

If you know that you are targetting a particular backend, you may wish
to also modify the grammars that control pretty-printing.

For the moment, just use the identity update in all our backends, so
that nothing changes in terms of what the user sees.

Make case-expressions in set comprehensions print with parentheses.

The way this is made to work is rather hackish: every possible case
expression in a comprehension gets parenthesised, even if it won't
cause a parse error. I don't expect there are many such in any case.

Replace add_ann_string with a more general add_xstring

Allows a custom size and/or annotation to be given to a string for
pretty-printing. For code using add_ann_string, you can get add_xstring
instead and define
fun add_ann_string s = add_xstring {s=s,ann=SOME ann,sz=NONE}
for an easy upgrade.

Significant change to pretty-printing; affects user-printing API.

The change allows user-printers to alter the main printer's notion of
what is a "seen free variable", and what is bound. The latter causes
the colouring. The first notion is important when show_types is on,
as types are only given for the first occurrence of a free variable.

This allows the monadsyntax to do the right thing with the colouring
of variables.

Added styles to the pretty-printer.

The recent changes to the pretty-printer use colours to convey extra information
about terms and types as they are printed. This is done via annotations containing
semantic information. For example, an annotation states that some string
represents a variable of some type. It's then up to the backend how to use
this extra information for displaying.

This checkin adds a concept of "styles". In contrast to annotations, styles express
formating instructions. A style states instructions like: "print the following in red and bold".
There are two new function: begin_style style_list and end_style.
Everything that is outputted between calls of these functions, should be formated in the given style.
There are the following styles available:

Setting the foreground color to c: FG c
Setting the background color to c: BG c
Use bold font: Bold
Underline text: Underline

begin_style takes a list of these styles. Thereby, the colors c can be choosen from a
standard 16 color palette:
Black, RedBrown, Green, BrownGreen, DarkBlue, Purple, BlueGreen, DarkGrey,
LightGrey, OrangeRed, VividGreen, Yellow, Blue, PinkPurple, LightBlue, White

In order to provide begin_style and end_style to user defined pretty-printers, the interface of userprinter
had to be extended. Instead of getting two functions add_string and add_break, the userprinter now gets
a record of a lot of different functions. Old pretty printers have to be adapted by changing

fun myprint Gs (sys,str,brk) gravs d pps t =
let
open Portable term_pp_types
...

to

fun myprint Gs sys (ppfns:term_pp_types.ppstream_funs) gravs d pps t =
let
open Portable term_pp_types
val (str,brk) = (#add_string ppfns, #add_break ppfns);
...

If you want all the functions, you can use

fun myprint Gs sys (ppfns:term_pp_types.ppstream_funs) gravs d pps t =
let
open Portable term_pp_types
val {add_string,add_break,begin_block,end_block,add_ann_string,add_newline,begin_style,end_style,...} = ppfns
...

Modify the ability to add user-printers so that they're keyed off
term-matches (using first order term-matching). Also give the user's
function access to the relevant grammars, and to the "smart"
add_string and add_break functions that the system printer uses itself
to avoid symbol merging.

Added ability for users to add their own pretty-printers, tied to the type
of the term being printed out.