Make MoscowML failure to build quote filter fatal

Fix compilation of Holmake errors (seen in configuration)

Earlier claims of success in 1b1b3de67 must have been misled by me
working in a directory that had been primed by previous build
attempts.

Get new version of Holmake to build under Moscow ML

Update tags to label release as Kananaskis-13

Remove unwarranted claim that emacs mode works for XEmacs

Compatibility with XEmacs hasn't been tested in ages, and as XEmacs
seems to be getting very little development love itself, I don't feel
too bothered by this.

Don't suggest we can compile with Moscow ML 2.01

Now there is an immediate failure to configure if this is attempted.

We get into errors due to an inadequate basis implementation if we do.
This then allows simplification of the codebase, which tried to
provide a stripped down extension to the basis library.

Many options in Holmake get removed as a consequence.

Update release details in configure.sml files

These feed in to what is displayed in the interactive REPL's banner.

Changes to get Moscow ML impl. to build once more

Includes:
- deletion of unused TermCoding module
- correction of failure to build Holmake
- movement of HOLPP out of impl. specific directories; impl. specific
stuff now in PrettyImpl module

Try to find dot in user's PATH during configuration

If it is not found, say little about its absence on help-graph build
time.

Get Theory.dat file change to build under Moscow ML

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.

Move FNameToUnquotedDeps.sig into main Holmake dir

This makes it more explicit that the code is shared between Moscow ML
and Poly/ML implementations. (For the moment, the Poly/ML
implementation *is* just the Moscow ML implementation, but that is
about to change.)

Refactor code to better isolate call to unquote in Holmake

The only use under Poly/ML is as part of dependency analysis and this
can be eliminated by providing a Poly/ML implementation of
FNameToUnquotedDeps.

Incorporate new c/line option-handling into build

The build in relocation option doesn't do anything at the moment.

Get "build from graph" Holmake to compile

Poly/ML version fails miserably at boolScript hurdle however.

Give BuildCommand a shared signature

This code is called from the common code of Holmake.sml so it must
export the same signature whether it is in Poly/ML or Moscow ML. That
signature is useful documentation and sanity-check.

Implement a -n option for Holmake

This uses the new dependency graph technology. It doesn't look
particularly pretty at the moment, but

Holmake -n -q

should be useful. (The -q suppresses useless info about automatic
dependency analysis.)

Closes #283

Put a main around mosml's Holmake

This makes the Moscow ML version look more like the Poly/ML version.

Give HM_BaseEnv a signature

Purge Holmake.sml of much Moscow ML specific code

The Moscow ML stuff has moved into mosml/BuildCommand etc

Progress with github issue #77

Switch Moscow ML Holmake to GetOpt cline options

This is a precursor to merging more of the Poly/ML and Moscow ML
implementations, as per github issue #77

Make KERNELID variable available to Holmake

This is the value of the kernel option that was passed to build when the
system was built. The build program stores it in the filesystem in a
"canonical location", and this file is read by Holmake when it starts
up.

Next release will be Kananaskis-11

This commit starts release preparation branch.

use /bin/sh instead of /bin/bash (which is not available on all UNIX systems)

also, use cc instead of gcc (no need to compile HOL4 with gcc)

Implement (efficient) holdep lexing by hand.

Without using references (except in the side-effecting stream reading,
I suppose). In any case, performance in Poly/ML is much better (~4s
on my old Mac for holdeptool on the 30MB CakeML theory.sml file).

Includes some test-cases.

Do away with use of mosmllex and mosmlyac in Holdep.

These tools are too Moscow ML specific, and unnecessary given that we
have mllex available for all SML implementations.

Start compiling new Holdep code in Moscow ML configure.

Generate a holdeptool along the way. This examines a source file and
outputs all the dependencies it believes that source file might have.
Mostly useful for debugging.

Start to rationalise Holdep's interface.

There were some strange holdovers still in there from the ancient days
when it was a separate command-line tool. Aim is to ultimately drop
Lexer.lex and Parser.grm and replace those with the Holdep_tokens
lexer. I'm also only doing this to the Moscow ML implementation for
the moment with the ultimate aim being to have the Poly and mosml
implementations using the same Holdep code.

Change Kananaskis-9 into Kananaskis-10 in the relevant places.

Implement wildcard function for Holmake.

Closes #36

Updated version number in manuals, banners etc.

Allow user to configure location of dot tool for theory graph building.

The default is /usr/bin/dot, because that’s where it is on my Linux machine. If you need it to be somewhere else, create a config-override or poly-includes.ML file, depending on which ML you’re using.

Moscow ML configure wasn’t filling in the value of CC for Systeml.

This then resulted in a bad Makefile in examples/muddy/muddyC.

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.

Remove Poly-specific executables from bin/ when configuring with mosml.

Update version numbers now that K7 is out.

Fix: need to recompile Systeml check was wrong when basis2002.sml was updated.

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.

Bump version numbers - next release to be 'Kananaskis-7'.

Recompile mosml basis if Systeml changes.

Also move version detection trick later so that warning message on 2.01
doesn't get in way of reading automatic guesses about config constants.

New Holmake feature: check to see if it should be being used as builder.

If, as I do, you have multiple HOL installations on the same machine,
it can be a pain to remember to build things with the correct Holmake.
On the other hand, it's certainly convenient having a Holmake in one's
PATH. So, this change gets Holmake to determine if it should be the
Holmake being used, and if it thinks another Holmake should be being
used instead, that other Holmake gets called out to instead. This
"calling out" is done through Systeml.exec, so can even be across
Poly/ML-mosml boundaries.

There are two ways in which a Holmake can decide determine the correct
Holmake to be used. If it sees a .HOLMK/lastmaker file containing a
path, then this is used. This file is written to when a Holmake does
decide it's the rightful make executable. Secondly, if Holmake
determines (by jumping up through the file-system) that it is being
called inside a HOL installation already containing a bin/Holmake,
then that is taken to be correct.

When a second Holmake is called as part of this process, it also gets
passed the --nolmbc flag ("no last made by check") to stop it going
through the whole process all over again.

Apply bits of Thomas's last Emacs mode update (7597) that are OK.

Revert "Added support for calling Holmake to hol-mode. Moreover, ..."

This undows commit 7597, which (unintentionally) undid changes of mine
in 7498. I will re-apply those parts of 7597 that are not broken in a
follow-up.

Added support for calling Holmake to hol-mode. Moreover, some more key-combinations were added.

Emacs HOL mode: now has a customisation group. If you do M-x
customize, and then select External/Hol, you will get the standard
emacs interface for changing some bits and pieces. Also add the
ppbackend toggle to the HOL menu. (This HOL menu should really only
appear above relevant buffers, not all the time.)

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.)

Make our copy of mllex use the 2002 Basis Library.

Make the basis hack for Moscow ML correctly identify which version of
the Basis Library we are trying to emulate.

Fix the issue of a fresh install of the quote-filter not working.
Ensure also that all future attempts to compile the quote filter will
appear fresh by calling Holmake cleanAll in the directory before doing
the compilation. (It was this that caused me to miss the compilation
error.)

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).

From now on we're in the Brave New World of Kananaskis 6.

Make configuring for use with Moscow ML cope better when this is
happening over an installation that used to use Poly/ML.
Interestingly, nothing needs changing if moving in the other
direction. Note though that in both cases, you will need to do a
bin/build cleanAll after configuring.

Start to factor out some code from build.sml that can be built in both
Moscow ML and Poly/ML so that it can then be shared between both
implementations.

Bug fix: delete a stray space character.

Put a variable ML_SYSNAME into the Systeml structure recording what ML
implementation is being used.

Make the organsiation of the mllex source-code a bit cleaner so that
the polyml version can be built more easily. If you have polyml
installed nicely, it should be possible to get a poly version of mllex
by just going
make -f Holmakefile mllex.exe
in the tools/mllex directory. The tricksiness in Holmakefile is more
cute than useful, as it's not used by Holmake.

* Changed Systeml to make it more compatible with the Basis Library,
in particular, by using OS.Process rather than just Process, which
is a MoscowML invention dating back to the times when it couldn't do
nested structures
* This has knock-on effects in a surprising number of places because
Moscow ML doesn't know that OS.Process.status is the same type as
Process.status.
* Also invent a PreProcess structure just to store isSuccess which is
in the most recent Basis, but not Moscow ML.

Fix the reference to Muddy so that it points at its new home in the
examples directory.

Remove one of the last remaining vestiges of "hol98"; in the Emacs mode.

Bugfix: remove a reference to Holmake_tokens.sml, which no longer exists.

Rework lexing of Holmakefiles so that the system doesn't choke on
Joe's monster example. The result is simpler code (which is a bit
worrying in itself), and one less dependency on mosmllex. It
successfully reads all of the distribution's makefiles, as well as
Joe's.

The system version and release information now comes from configure.sml,
which fills in the Systeml file, which is then available not just to the
standard source hierarchy but also to tools like Holmake and others.

----------------------------------------------------------------------
Enter Log. Lines beginning with `CVS:' are removed automatically

Committing in revisions to support XEmacs as well as Emacs.
The tools/hol98-mode.src file now should work for both editors.
There are two new functions early in the file that should be used
in the future for either detecting if a region is selected, or
turning on the selection. This has been tested, and I think it's
solid, but if anyone has problems, please contact me.

Modified Files:
configure.sml hol98-mode.src
----------------------------------------------------------------------

Get configuration to remove old quotation filter from bin directory before
proceeding. This stops Holmake from using the old filter when it compiles
the new one (and when it compiles things like mlyacc).

Modify configure so that it builds mlyacc. Also get the build process
to copy the mlyacclib object files into sigobj.

Some last minute changes to get release to work.

Last change I want to make before releasing; change the MOSMLDIR value
to be the directory containing the mosml binaries, rather than being
the parent of this directory. This should make life easier on those
installations where the mosml install doesn't look like
mosml
+----- bin
+----- lib
(Some do not have bin and lib as siblings. The code using MOSMLDIR
never looks for anything except bin underneath it.)

Updates (to code and documentation) to better handle situation where
dynamic linking is not available. Now, the Systeml structure records
whether or not it is by storing a boolean in the variable DYNLIB.

Check-in to get macosx recognised as a valid OS.

Update to the configuration scripts to support compiling Muddy on MacOS.
Thanks to Georg Weissenbacher for the information on how to do this.
(If someone has a mac, could they test this please?)

Undoing Anthony's change to configure.sml, which must have been unintended.
Anthony: you should be using the smart-configure.sml script, possibly
extended with a config-override file. See the install.txt in the top-level
hol directory for instructions.

Added FULL_STRUCT_CASES_TAC. It is the based on STRUCT_CASES_TAC - but it
updates the assumptions.

Changed the lexing implementation in src/parse to use our own copy of mllex.
Speed is comparable, code is conforming SML, and mllex is also something
of a standard for the other implementations too. I will eventually remove
all uses of mosmllex and mosmlyac from the distribution, perhaps starting
with tools/Holmake.
Functionality is slightly altered: it is now not possible to have
antiquotations inside comments. If there is hue and cry about this, I can
restore this functionality though in rather a hackish way. None of the
core distribution relies on being able to do this.

----------------------------------------------------------------------
Committing in the tools/configure.sml file.
Found an error in the part that sets the default value of the
"hol98-executable" variable when invoking HOL under emacs.
This variable was being set to the "hol.unquote" executable, which no
longer exists. I changed this to the "hol" executable, which is the
same one as before, but whose name has been changed for this version.

Modified Files:
hol98/tools/configure.sml
----------------------------------------------------------------------

HOL executables now named as Konrad suggested a little while ago: the
default hol include bossLib and ``..`` quoting. The version without
quoting has "noquote" appended to the name. You need to rerun configure
to see this change, but do not need to rebuild.

I realised that time-zones meant I'd be first in on Monday, so I've made
the fix to configure.sml. I've also documented the new configuration
method in install.txt and the TUTORIAL.

Small changes for understandability of configuration.

Sick of having to constantly edit configure.sml, I came up with a solution
last night that I hope is an improvement. Now instead of
mosml < configure.sml
do
mosml < smart-configure.sml
and it figures out the parameters for you. In order to figure out holdir,
you have to invoke the above either in the tools directory or in the
root hol directory. I believe it should work under windows too. (Some-
one with a Windows HOL, please confirm!)

I foolishly overwrote tools/configure.sml with my own setup, so I'm
fixing it here, but fixing it to do more in the way of error detection.

Got rid of QConv, and made all conversions do the "raise exception to
indicate reflexivity" thing. (Also fixed bug in new implementation
of ABS_CONV that attempted renaming on failure of conv, and not just
failure of ABS.)

Next step will be to rework the simplifier's implementation so that
it also uses Conv.UNCHANGED, rather than in its own internal version
of the same. This will let the simplifier play efficiently with
others.

May also assess making ABS_CONV not do renaming, and give the rewriter
its own special traverser. This might make some things more efficient.

Needed to compile the new version of Holmake.

Fairly drastic change to the way in which Holmake interprets Holmakefiles.
These can now contain arbitrary variable definitions and references, just
like in normal make-files. Rules can also use have multiple targets, and
the special variables $< and $@ have the appropriate meaning. These are
Feature Requests 597666 and 597668. I will attempt to document the changes
more thoroughly in the DESCRIPTION.

Modified to get rid of unnecessary .src file (and associated configuration),
given that we can just have Unix filenames with .exe extensions.

Blank out OS field in the same way that we blank out mosmldir and holdir
fields.

Fixes so that Holmake looks at bin/quote-filter.exe on w2k, instead
of bin/quote-filter.

More purging of the evil string "hol98"

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.

Fairly radical change. Now all of the "build-time" constants (such as
HOLDIR, MOSMLDIR and things like that) have been moved into the Systeml
file that is built and compiled as practically the first thing that
configure.sml does. This change means that we don't need to specially
generate Holmake.sml, Globals.sml, makebase.sml or build.sml. All of
these files can now just refer to Systeml. (In order to bring this
about for build.sml, I've also shifted the SRCDIRs variable to build.sml.
It had been in configure.sml just so that it could be copied into build.)

Added a comment in an attempt to make Windows users' lives easier.

Don't attempt to be clever with not recompiling Systeml. Do everything
the long way, and abort sooner if things have gone wrong.

Configure script now fails immediately if building Holmake or bin/build
doesn't work.

Forgot to use absolute directory reference and a bug resulted.

Modified configuration process a little. Now, the system specific cruft
is all stored in Holmake/$(OS)-systeml.sml files. These are moved over
Systeml.sml as part of the configuration process. Then other files that
depend on these bits and pieces can just refer to the Systeml structure,
and the amount of text copying can be reduced. configure.sml is also
now a bit less wordy by using quietdec := true.

Updated a lurking version number, and also modified the configure script
to put a "I am automatically generated" warning at the top of
help/src/makebase.sml.

Added word32 to the sources.

Made the wrong file executable (the script in the quote-filter directory
rather than the copy of the script in the bin directory).

Modifications to compile the quote-filter from the tools directory, and
to thus ignore the nasty C code in the quote-filter directory entirely.

Range of changes. Help system now generates and indexes ASCII versions
of .doc files, so that online help looks a fraction nicer. Doc2Txt
program in help/src does this translation. Elsewhere, I have removed
quite a lot of output from the building help phase of bin/build.
Errors are still reported, but successful translations, parsing etc
are not. Blessed quiet.

Putting back configure, after I just accidently committed my own version.
(I realized my mistake too late, and then used `!' instead of `a' to abort!)
Sorry if it broke anything else.

*** empty log message ***

configure.sml changes to include new marker directory as part of
build sequence, and also to slightly alter what happens when the help
system's makefile is built.

build.src changes to check both configure.sml and build.src before doing
a build.

Holmakefile.help.src changes to reflect new Doc2Tex tool.

Fix to let help system build on W2K (tedious business with .exe suffixes).

Fixed build.src to work on NT. This required changes to configure.sml
and the config- things. I'm not sure why std.prelude.src was changed.

Moved ring directory earlier in the build sequence so that my integer
decision procedures can exploit the normalisation code.

Had checked in version with my local information; oops.

Fixed some errors arising from the merge process.
Note that if you are using systeml in configure.sml (and there isn't
really any alternative), you can't do things like
systeml [cmd, "-opt1 -opt2", filename]
it has to be
systeml [cmd, "-opt1", "-opt2", filename]
(as per my mistake with -standalone -o below).

Changes brought across from Taupo-6 branch to make building and configuration
work properly under Windows. Significant thing is introduction of Systeml
module in Holmake directory which implements something of type
string list -> status
for executing commands using the O/S command interpreter. Special magic
in this module attempts to ensure that things will work even in the
presence of spaces in directory names (prevalent in Windows; possible in
Unix) etc.

Change to the start-up behaviour of HOL. At configuration time
the following 4 scripts get placed in the bin directory (as well as
a few others, e.g., Holmake):

hol -- loads and opens bossLib
hol.bare -- loads and opens boolLib only
hol.unquote -- the hol script, input passed through quotation filter
hol.bare.unquote -- the hol.bare script, using quotation filter

Most of the time, the hol or hol.unquote scripts offer the "right" context
for people to start working in.

This is tentative: I may change the names of the scripts
(suggestions welcome), or increase the libraries that the
hol/hol.unquote scripts load and open by default.

config-muddy.sml has been incorporated into configure.sml

Fixed so that filter.c is built (using make) if possible. Our release
practice to date has been to distribute filter.c in releases, but this
should be helpful for developers, particularly when getting started
with a fresh CVS checkout.

Actually, help/src/Holmakefile didn't need to be generated because
Holmake (now) understands MOSMLLEX and MOSMLYAC commands within
Holmakefiles. So I've put back help/src/Holmakefile and removed
tools/Holmakefile.help.src instead.

Removed MJCG's paths

Added HolSatLib

Moved predicate set development to be earlier than integers. This
allows Cooper's algorithm to use sets.

New support for the help system.

New help dbase support.

Needed to make this dependent on the value of HOLDIR.

New configuration of help system. Now the help system will get built
at the end of all libraries, automatically. One can also go

build help

as a separate invocation. This will build the help database and
lots of HTML stuff.

I hope this finally puts that mangled previous version to rest.

Corrected bug, caused by confusion as to whether or not systeml was
introducing spaces between its arguments. Made it so that it did,
as this is much more natural.

This should work ...

New small changes re:help system.

Forgot to check this in. Puts hol88Lib back in the loop.

Changes for paired syntax, plus opening Parse in std.prelude.

Kananaskis changes:
* Holmake build process slightly more involved because of support for
Holmakefiles.
* some theories/libraries now commented out of the build process,
e.g. set, tree and ind_def because these are being retired.

Added help database build phase to end of configuration.

Added Joe Hurd's prob library.

Moved tautLib to be much earlier in the build sequence. It doesn't
depend on anything more than basicHol90Lib, so may as well as be
as early in possible. In particular, this allows the simplifier
to use tautLib in the implementation of UNWIND_FORALL_CONV.

Blathat....

Ack!

Changed build order, and also fixed potential problem in installation
of quote filter on Windows NT (it's now copied from src/quote-filter
rather than being moved from there).

Some fixes to the way the quotation filter gets installed on
winNT. Formerly, it was being moved from src/quote-filter to
bin/unquote.exe. However, that could only be done once, so an
attempt to re-build the system after a failed build would certainly
fail (not being able to find src/quote-filter/hol_filt.exe).

Not sure about what this change was.

Upgrades to simplify the incorporation of external tools into the release.

Upgrades to handle external tools slightly better.

Slight changes.

Added lazy list theory to build sequence. Removed -standalone option to
call to compiler when building Holmake.

Yet more fixes in order to get the Windows build to work.

When generating the script to run hol.unquote, can't just have a file
name of the form dir/dir/dir, but must instead translate those forward
slashes into back-slashes. Further, don't bother trying to compile
quote filter code on Windows; instead just move executable into
position.

Fiddled with configuration files in attempt to get muddy to build under
Solaris, which it should.

Deleted robdd library.

Deleted src/res_quan/theories.

Changes due to the incorporation of John Harrison's datatype definition
package.
In particular, most of datatype moves earlier in the build sequence. The
old (and deprecated) bits stay where they were.

Added HolBdd to configure.sml and changed documentation-directories to
know about new location of reduce and arith libraries.

Reorganizing system so that reduce and arith are part of numLib.

Added HolBdd to the system.

Undoing fixed file names.

New library directory "basicProof".

Fixed order so that record types built before datatype.

Minor editing changes.

Needed a space after the `$*' emitted in the bin/hol script.

Changes to make the start-up banner look nicer.

Fixed to build all of Holmake, including calls to mosmllex and yac.
Also handles errors in build process by bailing out immediately.

Holmake is no longer dependent on the SRCDIRs of the HOL distribution;
it only needs to know where the sigobj directory is.

added the ring subdirectory

Undoing last change to configure.sml, which made my paths part of
the standard configure.sml.

std.prelude.src changed so that Psyntax and Rsyntax are both loaded
on startup. Psyntax is open by default.

lite and ho_match have been removed and are now part of basicHol90.

This allows tactics in basicHol90Lib to use higher order matching. The
only example so far is PAT_ASSUM, but there may come to be others.

Changes which represent a slight re-organisation of the way in which
hol.unquote starts up. It now reads a file called unquote-init.sml
from the tools directory. This file redefines "use" (this file is
kept separate though, so that others might use it if desired), and
also sets the term and type pretty-printing suffixes and prefixes to
be appropriate for the hol.unquote environment.

added src/sompute/src

Added error message for when quotation filter is not put in the right spot.

Additions for the new Muddy BDD package.

Changes to build order, plus minor tidying up.

New initialisation of std.prelude now figures out the documentation
directories by reading a file, which can be independently maintained, and
which can also be used when the help and index files are themselves built
(see developers/help).

The replacement routine in configure has also been slightly changed to
make it more robust in the presence of edits to std.prelude.src; where it
used to insist on a line being exactly equal before it would replace it,
now it just requires the redex string to be present before replacing.

Globals.src : upgraded version to Taupo 1
configure.sml : changed the order that SRCDIRS are taken in
std.prelude.src : added "via" (from Tactic) as infix operator
use.sml : cosmetic changes

Blanked out mosmldir, holdir and OS fields with underscores.

Changes to accomodate MoscowML 1.44 release.

Extensions to include the robdd library in the standard build process.

Put version back into repository that has underscores for mosmldir and
holdir.

*** empty log message ***

Put generation of hol98-mode.el under control of configure script.
Checked in configure.sml with initial values of holdir and mosmldir set
to underscores.

Modified to build datatype/record after datatype/ so that the record
definition can take advantage of the TypeBase changes in Datatype.Hol_datatype.

Trivial changes.

Fixed to bring it up to date with Taupo release 0.
(Changes have come across from parse_branch development.)

Modified pretty-printer installation to make the installed printers
catch exceptions. Failure to do this tends to crash the interactive
system, which is a bit serious.

Initial revision