Apply the quotation filter to all input files

Previously, a has_dq (“has double quotes”) function was applied to
test files to see if they should be filtered. With Theorem syntax used
in files that didn't include any Unicode or backquotes, this analysis
was wrong. Nor is there any need for it. It's simpler to just apply
it to everything.

Provide facility to learn where a file was loaded from

Tell load about more Basis modules that are already "loaded"

The emacs mode tries to load these modules when it sees them used, but
this prompts an error, because the load machinery doesn't know they're
built-in and then tries to find the source code for them and fails,
emitting an annoying warning.

Attempt to manage all heap interactions in one executable

System builds non-interactively, but the interactive REPL is broken,
as are selftest.exe files after hol.bare.

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.

Write and read .uo/.ui files using the $(HOLDIR) variable

This should make HOL installations portable (once heaps are rebuilt).

Let .uo and .ui files have $(envvar) prefixes in their paths

This will let these files specify positions for source code that is
independent of an absolute position in the file-tree hierarchy, but is
relative to a fixed base. The first step is to allow $(HOLDIR) so that
HOL can have its own .uo files be easily relocatable.

Next step is to write .uo and .ui files using this facility.

Allow buildheap to create heap with timestamp in past

This is under control of an environment variable for the moment. This
is because I don't want to change Holmakefile command-lines, but do
want to be able to run buildheap in a context where heaps get rebuilt
in this way.

Rework Poly/ML quotation use to do in-process lexing

This changes from having to use a separate unquote process as part of
Holmake, and may help resolve github issue #340

The drawback at the moment is that the whole file is sucked into memory
before Poly/ML gets to see it. The way the filter code works
could (should?) be changed to lex things in a demand-driven way.

Remove a race condition in the file system

The quse function may be called simultaneously in two different
processes on the same file, making them contend for the file
.HOLMK/originalname; this leads to errors. Now use tmpName (which is
not immune to racy problems), which is an improvement.

Let load work if current directory is unwritable

Better errors when use can't make a .HOLMK dir

Get Poly/Holmake to apply the quotation filter to more files.

The Moscow ML implementation just applies it to everything (and
perhaps the Poly/ML implementation should do the same). The new
behaviour in the Poly/ML code is to apply the filter if the `
character is detected, or if any character with code > 127 appears in
the file to be consumed.

Curiously, the quotation filter is applied within Holmake under Moscow
ML, but within the load implementation in Poly/ML, and this lives in
tools-poly/poly/poly-init2.ML. Because it isn't used in
tools-poly/Holmake.sml, I can delete some redundant code in

The test-case exercises this because it uses only "new style"
quotations (enabled by 199f6f07d0).

Make interactive Poly sessions know that Listsort module is loaded.

Stage the Poly/ML interactive system to know about built-in modules.

In particular, Binarymap is built-in from the very start, and PP (an
overloaded name for HOLPP) is available once the kernel is loaded.

Give temporary files used by Poly/ML nicer names.

This is done by creating the files (the outputs from the quotation
filter) in local .HOLMK directories but with the same name. Then error
messages are easier to relate back to original source files.

Closes #32.

Make Systeml.sig the same in Moscow ML and Poly builds.

This additional uniformity allows me to delete the
tools-poly/Holmake/Systeml.sig file. This then requires a bunch of
changes to compilation of the early tools which have to point at
tools/Holmake/Systeml.sig rather than the version in
tools-poly/Holmake.

This should fix the configuration errors on MoscowML introduced by
0a0988fc.

Allow Moscow ML build to happen using (as yet unreleased) v2.10.

Basic strategy is to make adoption of basis 2002 even more
thorough. In particular, the Timer structure is now as per
the 2002 Basis.

It is possible to detect that one is working with Moscow ML 2.10 or
later by checking the Holmakefile variable $(HAVE_BASIS2002), which is
set (to value "1") when in 2.10 or later. It is unset elsewhere. See
an example of its use in help/src-sml/Holmakefile.

Minor tidying in Poly implementation of load/use.

Fix startup problem for Poly/ML HOL (caused by recent Holmake refactoring).

Moved a bunch of things from tools-poly/poly to portableML/poly.

Still to do: make Poly Arb{int,num} use Poly's built-in arbitrarily
large integer type. Also want to get rid of the last remaining
"redirect" in tools-poly/poly/poly-init2.ML.

New "portable" subdirs per ML implementations in src/portableML.

Hope to do away with Poly/ML specific code in tools-poly eventually,
moving it into src/portableML/poly. tools/build-sequence now records
that the implementation-specific directories have to be included.

Make quse emit an error message on failing to find a file.

The exception that it otherwise raises can cause "invisible" failures
when doing a Holmake. I presume that the exception is occurring and
that this is aborting the Holmake and the build, but nothing gets
printed so it can be hard to know why the build has stopped.

More changes to get basis2002 changes working properly in both poly + mosml.

Implement more of Basis2002 for Moscow ML (adding Vector, Array,
ArraySlice and VectorSlice), simplifying what Poly/ML has to emulate.
Haven't done full rebuild test, but have got as far as integerTheory
and Omega, which makes heavy uses of Vector etc.

Move the pretty-printing facilities around a bit so that both SML
implementations use our own version of the PP structure. This
implementation is called HOLPP in src/portableML. After the kernel's
Overlay.sml is loaded, it is also available under the name PP. This
retains fairly good backwards incompatibility. The one deliberate
incompatibility is to make references to General.ppstream invalid.
This makes us better conform with Basis 2002.

The advantage of this manoeuvre is to allow me to better control what
our pretty-printers do at a low level.

Update us to use the Basis2002 version of Word8Vector. Seems to
affect only src/parse/CharSet.sml. (Changes to tools/configure.sml
make it better at detecting situations where basis2002.{uo,ui} need to
be transferred to sigobj.)

Start to implement the Basis 97 extensions that Moscow ML hasn't got
in order to force our codebase to get up-to-date. It should also
mean less bodging around for the Poly/ML code. I haven't checked that
my changes to tools-poly/poly/poly-init2.ML have done all that is
required yet. Feel free to fix problems arising there (I hope it will
just be a matter of deleting things).

OS.FileSys.tmpName () creates the temporary file on PolyML (as the basis spec
says it should), so do a better job of deleting them.

Set the emulated list of loaded structures to include Int, Real and
List. This should stop the system getting all twisted and bitter when
the Emacs mode asks the REPL to load these.

Update to work on Poly/ML 5.2 (which breaks 5.1 compatibility).

The ARM examples now work on the Poly/ML version.

A fix to load.

Set Globals.interactive properly under Poly/ML.

More tweaks to the Poly stuff.

Misc fixes to Poly ML compatibility.

PolyML compatibility. See tools-poly/README.