Now up to type pretty-printing

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

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

Move type antiquotation stuff from term_pp to parse_type.

Separate pretty-printing code into two halves, with a backend
component able to provide special treatment of the basic
pretty-printing functionality. The front-end can call a special
version of add_string in order to let the back-end know that a certain
piece of text has special properties. The handling of the given
annotations is up to the backend.

The raw_terminal backend ignores all annotations.

The emacs_terminal backend is the same as the raw_terminal backend for
the moment because I can't figure out how best to pass information
on.

The vt100_terminal backend colours free and bound variables blue and
green respectively using ANSI/vt100 escape codes. You should see this
if you start up HOL in an xterm (or gnome-terminal, or ...).

The current_backend reference variable in Parse can be set to alter
the backend being used for printing. For example, if you do

Parse.current_backend := PPBackEnd.vt100_terminal

while running in emacs, you will see your terms mangled with lots of
\^[ type junk.

I think a LaTeX backend should be possible, as might some sort of XML
or MathML thingy.

I suspect my token merging avoidance code will need updating.

Also, change std.prelude to set the interactive flag earlier, so that
Parse can see it (it will use raw_terminal if loaded non-interactively).

Make symbol-merging be avoided by default. Also ensure that (* and *)
tokens are not created by separate calls to the printer. Remove the extra
"setting" and "getting" functions in Parse.sig that Peter introduced
because I think they are now unnecessary. (Feel free to put them back
if they are still needed for your application Peter.) There is now also
a flag that can be set to level 0 to get back the old behaviour of the
printer, though I can't imagine why anyone would ever want it.
This implementation does not attempt to create a new ppstream - instead
the "wrapping" happens above the PP calls that are made in term_pp. In
particular, add_string and add_break are masked by calls that share a
reference containing the last outputted character. The problem with
creating new ppstreams is that you end up with multiple copies of state
representing the "same" state of the output page, and this leads to
formatting errors.

----------------------------------------------------------------------

Committing in new ability to create and use safely printing ppstreams.

This provides a new term printer term_pp.pp_term_sep to enable better
separation of symbolic identifiers when printing terms.

However, to activate this, one must create and use a new ppstream which
has as its consumer function one which was wrapped by the function
term_pp.wrap_consumer_sep.

Example:

val normal_grammar_term_printer =
Parse.set_grammar_term_printer term_pp.pp_term_sep;

val linewidth = ref 75;

fun mk_sml_ppstream f =
PP.mk_ppstream {consumer = term_pp.wrap_consumer_sep (fn s => TextIO.output(f, s)),
linewidth = !linewidth,
flush = fn () => TextIO.flushOut f}

Then printing with mk_sml_ppstream should separate symbolic identifiers.

It's not a beautiful solution, but it works. Improvements are welcomed!

Modified Files:
Parse.sig Parse.sml term_pp.sig term_pp.sml
----------------------------------------------------------------------

Make case-expressions print out much nicer. Thanks to Anthony for prodding
and to Konrad for mentioning the availability of TypeBase.strip_case.
Also make case constants that are not partaking of special case syntax
print out with their underlying names, rather than just "case". The effects
of both changes is visible here:
- ``case ell of [] -> 3 || (x,y)::t -> x + y``;
> val it = ``case ell of [] -> 3 || (v2,v3)::v1 -> v2 + v3`` : term
- dest_term it;
> val it = COMB(``list_case 3 (\v v1. case v of (v2,v3) -> v2 + v3)``,
``ell``) : lambda

Two changes.

1. Moved definition of ty_antiq to Parse so that it will
appear in the docs. Other changes arose.

2. "Fixed" HolCheck so that it builds. Is this a
difference between the std and expt kernels?
The change swaps type variables in arguments to
type operators so is probably not what Hasan had
in mind.

Implementation of "parse only" type abbreviations. The main function to
use is type_abbrev : (string * hol_type) -> unit

If the hol_type has type variables in it, then these become parameters to
the string, making it an abbreviation for a type operator. E.g.,
type_abbrev("set", ``:'a -> bool``)
allows you to write ``:num set``.

No attempt to pretty-print types in accordance with stored abbreviations,
so the system will spit back ``:num -> bool`` in response to this. (Hey,
if it's good enough for Moscow ML, it's good enough for us.)

Also split off type_grammars into their own source module.

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

Support for new representation of strings.Minor changes.

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.

Added .sig file to type_pp.
Fixed bug which was pretty-printing :(bool |-> bool) |-> bool without any
parentheses.
Removed some spurious reference variables from term_pp.

Small changes to accomodate new-look of portableML.

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