Hol err datatype

[konrad-slind]

Improvements to HOL_ERR. Currently HOL error messages get unnecessarily repeated as various layers of handling unwind, both in the REPL and in batch mode. This PR changes the representing type for HOL_ERR to be a 1-constructor datatype wrapping the current record type, then adds a prettyprinter for the datatype. This lets the REPL print HOL_ERRs that propagate to the top level only once. For batch processing, the original HOL_ERR can be printed and then further error messages are minimized.

There is still some fine-tuning to be done on the look-and-feel of messages, in particular for "user-facing" tools. For example, type inference failures are annoyingly repeated, as are other parse failures. I also haven't looked at whether the inductive type definition failures need cleaning up.

Not sure how this will impact CakeML. Hopefully not much

[konrad-slind]

Ouch. Selftests are failing because of a change to the batch-mode error reporting. Will be a few days before I clean this up. But a bin/build at level 1 works fine, should anyone want to have a gander.

[konrad-slind]

This is now ready. There weren't many problems with the selftests. I haven't looked at MoscowML.

But, as I wrote above, at least two things need to be improved once this change is (I hope) accepted.

1. Type inference error messages
2. The distinction between "repl_mode" and "batch_mode", ie, whether Globals.interactive is true or false, needs to be propagated more widely. For example, the possible exceptions coming out of the "events" of Modern Syntax (Definition, Theorem, Datatype, (Co)Inductive, etc) need to be treated differently depending on which mode the system is in. Thanks to Michael's previous work, Definition is largely taken care of, but for Theorem I need to look for something named (guessing) located_prove_thm or some such.

The mode distinction and its treatment is straightforward (Michael's code):

fun render_exn srcfn e =
    if !Globals.interactive then
       raise e
    else
      (output_ERR (exn_to_string e);
       raise BATCH_ERR srcfn)

Basically BATCH_ERR is used to avoid being caught by HOL_ERR handlers, which result in tedious replication of messages. It's used in situations where an excellent top-level error message has already been printed, so any further messaging is just annoying.

... Having looked at it a bit more, I wonder whether the invocation of render_exn on Modern Syntax elements should be done in the SML definitions ultimately invoked, or when HolParser runs.