Move DefnBase to src/coretypes, make progress with one_line_ify

DefnBase is now home to the updated literal-decider conversion

Reinstate (short!) message about changed loadPath when hol begins

(This fixes Moscow ML interactive behaviour to be the same also.)

Update Moscow ML's std.prelude for change in ReadHMF API

Get Moscow ML interactive p/printing to work

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.

Provide p/printer for rules part of a term grammar

Closes #249

Add print_banner function to interactive preludes

This allows the banner to be printed in other contexts if desired.

Interactive prelude now displays "how to quit" advice as it starts.

Make interactive HOL pay attention to PRE_INCLUDES variable.

Holmake was already doing the right thing here.

(PRE_INCLUDES allows users to re-use names for theories and modules
that the core system already used. However, this is not perfect in the
presence of preloaded theories that occur in standard heaps. In other
words, I doubt we will ever allow users to override "listTheory", for
example.)

Get Moscow ML's std.prelude to work with new Holmake modules.

Move kernelid variable to Thm so that it isn't shared across kernels.

Thanks to Anthony for spotting the problem.

Move name-of-kernel string variable (kernelid) from HolKernel to Theory.

Create kernelid variable in HolKernel to identify which kernel is being run.

Display this in the interactive start-up banner.

Set up a facility to allow configuration of interactive sessions.
When the interactive session starts up, it looks in the user's HOME
directory for files called
hol-config.sml
hol-config.ML
.hol-config
.hol-config.sml
.hol-config.ML
If any of these exist, the first that does is "use"-ed into the
session.

Renamed help/Docfiles/README.Hol98.

Separate pretty-printing code into two halves, with a backend
component able to provide special treatment of the basic
pretty-printing functionality. The front-end can call a special
version of add_string in order to let the back-end know that a certain
piece of text has special properties. The handling of the given
annotations is up to the backend.

The raw_terminal backend ignores all annotations.

The emacs_terminal backend is the same as the raw_terminal backend for
the moment because I can't figure out how best to pass information
on.

The vt100_terminal backend colours free and bound variables blue and
green respectively using ANSI/vt100 escape codes. You should see this
if you start up HOL in an xterm (or gnome-terminal, or ...).

The current_backend reference variable in Parse can be set to alter
the backend being used for printing. For example, if you do

Parse.current_backend := PPBackEnd.vt100_terminal

while running in emacs, you will see your terms mangled with lots of
\^[ type junk.

I think a LaTeX backend should be possible, as might some sort of XML
or MathML thingy.

I suspect my token merging avoidance code will need updating.

Also, change std.prelude to set the interactive flag earlier, so that
Parse can see it (it will use raw_terminal if loaded non-interactively).

Modify the initialisation of interactive pretty-printing in Moscow ML
so that the code in std.prelude doesn't need to be duplicated in
end-init-boss.sml.

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.

Add a pretty-printer for location values.

Debugging Preterm.sml made me write a pretty-printer for pretype
values (and I was almost annoyed enough to write one for Preterms
too). I use Moscow ML compiler magic to get numbers for references,
and have written to the Poly/ML mailing list to ask how to do the same
in poly.

The pretty-printer for grammars has changed, so the way HOL starts up
needs to change too.
(Forgot to check this in last night -- sorry!)

Add a pretty-printer for time values. (Only needed for Moscow ML,
Poly already does something sensible here.)

Modify the ability to add user-printers so that they're keyed off
term-matches (using first order term-matching). Also give the user's
function access to the relevant grammars, and to the "smart"
add_string and add_break functions that the system printer uses itself
to avoid symbol merging.

The Unicode module is loaded automatically; UTF8_Printing has gone.

Add some support for nice Unicode constants. Start up hol, type
UTF8_Printing.all_printing()
and then
pred_setTheory.IN_UNION

If you run HOL inside an xterm, you may need to have LANG environment
variables set. If you are using HOL inside Emacs, you will probably
need:
(setq default-buffer-file-coding-system 'utf-8)
(setq process-coding-system-alist '((".*" . utf-8)))
in your .emacs file.

Please experiment with making this nicer. (It may also be nice to
provide users with a way of backing out of this :-)

A whole mess of small changes intended
at making simpsets prettyprint informatively
in the interactive loop. Very possibly
I haven't updated all the files in the examples
directories.

Final bit of fussing with quiet declarations.

Realised that putting the quietdec thing into Systeml wouldn't work in
Moscow ML because this code needs compiling and you can't compile
references to the Meta structure. So, I just put it into the
respective prelude files.

Added proofManagerLib. This adds a type of "goal trees"
as an alternative to goalstacks. Relevant entrypoints:

gt ` .... ` -- start a goaltree proof,
analogous to g
eq ` ... ` -- expand a tactic,
analogous to e (except that
the text of the tactic is
delimited by quotes).

A goaltree manages the construction of the final
tactic, so should ease some of the script maintenance
that the goalstack requires.

Backup and restart are just as for goalstacks.

All the entrypoints for goalstacks are just as they
were before; there shouldn't be any difference.

Fixed syntax error in std.prelude. Not sure how that snuck in there...

Make a change I've long wanted: if hol is started in a directory with
INCLUDES specified in a Holmakefile, then put those same includes onto
the loadPath that is used interactively. This should help interactive
debugging of multiple-directory developments.

Get the Arbrat module loaded at interactive start-up.

Made a bunch of changes to the HOL source to make it more "Standard ML",
to make it easier to port to MLton.

For example:
+ Added lots of structure wrappers around miscellaneous .sml files.
+ The type of "before" is 'a * () -> 'a, not 'a * 'b -> 'a, as Moscow ML
currently thinks.
+ Added "val _ = " before random declarations.

A plea: if I'm ever going to succeed in porting HOL to MLton, could
people please stop using Polyhash. It's very useful, but there's
nothing like it in MLton (or indeed Standard ML). In theory I'm going
to have to change the (sometimes complicated) code to use Binarymap or
something like it, but in practice I'll only do that when there's
absolutely no other way.

Fix std.prelude; Konrad checked something in that was clearly a throwback
to a very ancient state, and which included a raw reference to his own
directory structure.

Added interactive loading of ML evaluators when standard HOL
is invoked. This is currently somewhat preliminary. After
HOL starts, you should be able to do stuff like

termEval (Term `2 + 3`)

and have the term be mapped to ML, evaluated, and then the result is
mapped back. There are also other entrypoints, see src/datatype/Interactive.

Overlay.sml now exports infix declarations for the "standard" infixes,
taken from std.prelude. This means that the infix component of the
standard Script boilerplate is unnecessary. Updated Manual documentation
to reflect this. Changed combinScript and examples/ind_def/clScript.sml
just to show that it worked.

Added THEN1 (Joe's useful "deal with just the top goal") as an infix for
the interactive system.

More purging of the evil string "hol98"

Resurrected this and modified the std.prelude to be able to find it, so
that when the user types help "hol" (as suggested in our banner) they
actually get something other than an error message.

Modifications to remove the need of std.prelude to be generated from the
std.prelude.src file. Also cleaned up the way the executables are
generated.

Recurring nightmare. I hope it stays removed!

Trivial changes. std.prelude should get removed from the archive, since
it is generated.

This is generated from elsewhere, so shouldn't be in the repository.

Initial revision