Provide a regression test entry-point for pretty-printing output

Occasionally bare strings can be annoyingly ugly

Avoid GC test warnings on low user times, and avoid a MoscowML bug

When MoscowML divides by 0.0 it raises Div.

Flag really bad garbage collection performance in selftests

If you get one red number attached to a fast test in a large series of
tests, this is probably not fair: the GC is probably happening to cope
with the whole series.

Improve printing of multiline pretty-printing test failures

Provide 'quietly' in testutils to shut up messages and warnings

This just uses Feedback's existing facilities.

Change testutils API to allow for counting of failures

Don't want to necessarily just always instantly abort. Changes die's
type from

string -> 'a

to

string -> unit

This causes a number of knock-on effects.

Make equality of "tight" precedence by default

Start to work through knock-on effects of this.

Make testutils.tprint remove newlines in string to be printed

In particular, if string to be printed is derived from a
pretty-printer (term's, say), then it may split a big term over
multiple lines and those lines then mess with pretty selftest output.
Instead, just replace newlines with single spaces.

Modify testutils.require_msg and derivatives to return values

It can be useful to get back the result of a passing test for use in
further tests that build on that.

Knock-on effects where it is now not possible to simply List.app such
functions; they must now have their results explicitly ignored.

Have testutils.die automatically print out "FAILED"

Argument to die is then appended to that, but on a new line.

Adjust some selftests to take advantage of this, though of course, we
don't expect to see the FAILED output for any of them because they're
all passing.

More tweaks to testutils

- change API of check_HOL_ERR to be tupled rather than curried (makes
it easier to write the (fn _ => true) predicate)
- add check_result entrypoint

Tweak testutils

- output on failures now prettier
- more utility functions
- make 'a testresult same as 'a Exn.result

Fix another conditional-expression p/printing oddity

The if-then- block wasn't necessarily aligned with the last else block
because the whole if-then-else wasn't guaranteed to appear in one
block to itself.

Closes #588

Also tweak error-reporting from testutils.tpp (use ␣ (U+2423) for
spaces to make spotting differences easier; control colours better).

Add testutils functions to make testing for expected errors easier

Use UTF8 functions for fiddling with strings in testutil output

Otherwise you can split UTF8 strings in bad places with functions such
as substring.

Make tty-output (Holmake and testutils) terminal-width aware

Holmake even checks for resizing every second so that long-running
jobs can have the terminal resized by the user and have the pretty
columns of jobs adjust accordingly.

Closes #526

Up to and boolTheory and slightly beyond

Give testutils some test-colouring facilities

Provide functions to make timing info easier to print in selftests

Add function for testing conversions into testutils

Make output in standard test of pretty-printing use Unicode quotes

Handle infix cons-operators (like pred_set$INSERT) better

Still can't get past the self-test in src/pred_set/src

Term-grammars now maintain their own max-timestamp so that successive
rules' timestamps are guaranteed to increase. (Previously, the new
timestamp just got made bigger than the timestamps associated with
"related" grammar rules. This required a scan of all the grammar's
rules, and a careful definition of what it was to be related.)

Add ability to add more text to test-diagnostic output

testutils.sml: flag for preventing die to kill HOL

While writing selftests, it may be useful to just raise an exception
instead of killing the HOL4 process in case of error. The new reference
"really_die" allows this.

Move Holmake & test verdicts one character left

This stops the rightmost character (the 'K' in 'OK', for example) from
being blanked by the clear-to-end-of-line formatting that gets output
after Holmake verdicts (as per 6828af9a21). If your screen is wider than
80 columns, you don't see this effect.

Move testutils to src/parse

It provides a convenient way to test pretty-printers, so depends on the
sources there.