Pretty printing error messages

[mtzguido]

This is still a draft, posting for opinions and comments.

This PR changes the error message type from a string into a list Pprint.document. This allows to present better messages to the user, as we can retain the indentation of printed terms, even with line breaks and the like. We can also wrap text to a comfortable line length.

I used a list to allow for several sections within a single error. We usually prepend some context to an error, or append some hint or range, and using just strings that gets pretty messy. Using a list allows to do that very easily by just adding a doc to the chosen end of the list. I copied a bit of the style from GHC.

Here's a small example of the difference, before (ignore the >>Got issues markers):

After:

Before with --query_stats and --error_contexts (just the tail):

After with --query_stats and --error_contexts (just the tail):

See ae1f869 for a complete diff of the error message expected output.

When in VSCode/Emacs, the messages are rendered before passing them to the editor. Here's an example from Pulse:

The Error <unknown> is a Pulse problem I think, in that it doesn't set the error number. I chose to display <unknown> in that case. Also note that I am displaying the "header" there since I didn't see the error number anywhere in VScode, and I think ideally the error should look exactly the same in both cases. But Emacs does display it, so we need to make a choice.

Pending:

• It's not hard to make the red/cyan coloring apply to only the Error/Warning part of the message, or to the header or whatever. Should we do that? The whole thing being red may be a bit too much, and also prevents coloring a part of the message if needed (e.g. if we want to highlight a difference, something that I want to do).
• Note that I kept the error context around, even if the message is now more structured. I see the context as a description of when/where the error was raised, while the message itself just contains pieces of information that the user definitely wants to see.
• I haven't translated all errors (or even a significant part) to using docs natively, but the SMT and tactics wrappers are now list-aware so they use that instead of concatenating strings. Also, all errors are now calling mkmsg : string -> error_message by default, so they get wrapping automatically. This is sometimes undesirable as it will kill the formatting of a term_to_string inside the error, so we should change them before merging.
• Fix the discrepancy between VSCode/emacs wrt the header.
• Expose the doc-list interface to FStar.Issue.fsti in ulib/. Currently userspace can only use strings, so formatting is lost.

[mtzguido]

I've been running this for a few weeks and I find it pretty solid. I also changed the interface of FStar.Issue to allow userspace to generate docs for messages, which Pulse can make good use of. I've removed the forced wrapping of messages, so messages that were not converted to the doc interface still look reasonable.

I'd like to merge this and tweak as we go, if others agree.