Tidy up polyscripter and turnstiles (in ##thm and normal contexts)

Workaround PolyML bug to print exceptions nicely in polyscripter

Tweaks to polyscripter, some revision of its selftest

Goal pretty-printing has slightly changed, so I adjusted the test in a
few places as those seemed to be places where the old behaviour wasn't
particularly worth preserving.

Make polyscripter tool pay attention to Holmakefile INCLUDES line

Refactor some code along the way so that this reading of Holmakefiles
is now a standard facility in the ReadHMF structure.

Test that it works by making the polyscripter test read from
examples/misc.

Adjust building of polyscripter for new buildheap process

Implement ##thm command for the polyscripter

As per the README, this allows for theorem values to be printed into
the output, indenting the value and losing the unnecessary 'val it ='
and ':thm' surrounds.

Isolate a simple buffer in Holmake code and reuse in polyscripter

Fixes previous commit's failure to build polyscripter

Implement parse{tm,ty} directives for polyscripter

polyscripter: truncate long metis: lines

polyscripter's ##assert shouldn't give blank line

Relax indentation rules for polyscripter commands

In particular, allow things like

>>__ val foo = ...
.. more text ..

Previously, polyscripter would delete text on following lines to make
everything line up with the "val" above.

Polyscripter dies cleanly if it can't open umap file

Remove more goalstack cruft in polyscripter

Yet another directive form for the polyscripter

Mimic Poly/ML's exn output better in polyscripter

add polyscripter command for catching and printing exceptions

polyscripter: add >>- for suppressing input but printing output

Allow polyscripter commands to be escaped

Handle indentation better in polyscripter

Fix polyscripter to not lose blank lines

attempt to allow indented input/output in polyscripter

Polyscripter: ##assert directive; work on parity chapter

Better elision of cruft in polyscripter

Make some things reference values so that they might later be
user-configurable from command-line etc.

Give polyscripter ability to silently 'use' files

Executable for running HOL sessions in text files

Lines not preceded with >> are passed unchanged to the output; lines
with >> are executed in a HOL session with the input and output of this
passed onto standard out. Lines with >>_ are evaluated but the output
is replaced by "output elided".