Add "quote fix" mode to unquote c/line tool

Now:

unquote --quotefix

filters standard-in to replace `` and ` with “ ” and ‘ ’ as
appropriate. Leverage the existing logic in the quotation filter so
that it doesn't get confused by characters in strings and comments.

Make polyscripter interpret text in "interactive" mode

This allows the Theorem/Definition syntax to be used in the manuals.

have QuoteFilter produce positions tracing back to the original source

Make QFRead API slightly narrower, but richer with it

In particular, provide access to a reset function that will reset the
state of the user-state component of the lexer. Unfortunately, this
does not include the mllex notion of state (<INITIAL>, <string> etc).

Get basic interactive executables to work

Implement line-number reporting for failing THEN1/>-

This relies on a somewhat disgusting quotation filter hack which
replaces occurrences of >-/THEN1 in line with the following pattern:

tac1 >- tac2 - - - > tac1 >>- linenumber ?? tac2

This relies on >>- and ?? being left-associative, which is how they
are defined. The definition of ?? is

fun f ?? x = f x

The linenumber is inserted by the quotation filter, which tracks this
naturally.

Implement rudimentary repl underneath buildheap.

Still need to arrange for the poly-specific prelude to be fed into it

Make quotation handling more efficient

In particular, dependency analysis on files does not need to read the
entirety of the file into memory first.

Isolate a simple buffer in Holmake code and reuse in polyscripter

Fixes previous commit's failure to build polyscripter

Make Moscow ML dep. calculation unquote-free as well

This allows yet more pleasant refactoring (with the
FNameToUnquotedDeps module completely disappearing). Now there is a
generally useful QFRead module in tools/Holmake that allows the
quotation machinery to be applied to strings and files.

The quotation filter is still a "push" technology: it consumes
everything it can and outputs as it goes. (It does block if its input
stream blocks of course.) I think it would be nice to modify the
filter (now QuoteFilter in tools/Holmake) so that it was "pull", the
client getting to pull chunks of output a bit at a time.

Currently, the API supports "reader" operations of type unit -> char
option, and these look like pull operations, but these are pulls on a
buffer that has already been filled with as much output as possible.