Get Moscow ML quote filter to build given bb2fff9e

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.

have QuoteFilter produce positions tracing back to the original source

Give standalone quotation filters option to control "interactivity"

Hitherto the form with no arguments

unquote < foo > bar

was "interactive", and the form with two arguments

unquote infile outfile

was not. Now add a -i option for the second case to make it
interactive, and a -n option for the first to make it not interactive.
Also give a brief usage message for a standalone -h.

Interactivity controls whether or not certain special forms that
should only appear in script-files (and when the interactive system is
being used) get transformed. In particular, this controls the handling
of >- and the new Theorem <name> <quotation> <tactic> syntax.

The Poly/ML version of unquote is not used within the system but gets
the same changes to behaviour just to keep both versions equivalent.

Get Moscow ML build to work again

Fix interactive unquote to handle Control-C better

In particular, it's possible to interrupt a quotation parse, and not
then be stuck in the state of quotation-parsing for the rest of the
session.

Make quotation handling more efficient

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

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.

Quote filter now outputs via user-provided fns

Previously it targeted a TextIO.outstream, only assuming output and
flush operations.

Minor tidying in quotation filter code.

Copy across Scott's poly code for the quotation filter to
tools/quote-filter, and then modify it for Moscow ML, as a prelude to
getting rid of the tools-poly version entirely.

Bug fixes for this new implementation.

Revised the quotation filter to use mllex rather than mosmllex. This
should help with portability.

Implementation of the quote filter purely within Moscow ML. This works
just as well on Windows, and has the added advantage that if in the middle
of typing in something with delimiters (such as a term or a string), then
hitting control-c causes the pre-processor to forget that that's where you
were and just bounce you back to the default top-level state. Hopefully
this will mean an end to having to type random numbers of ` and "
characters in desperate attempts to have everything match up.

Source code for a Moscow ML quote filter. Compiles and runs fine, but
doesn't have the capability to ignore interrupts at the moment, making
it useless for our purposes.