Add info about json, xml and clarify exceptions

Author: Sonny Martin

src/util/README.md

@@ -315,8 +315,8 @@ The deserialisation does the oposite process and it is implemented in
 \subsubsection irep-serialization-strings Serialization of Strings
 
 A string is encoded as classic 0-terminated C string. However,
-characters `0` and `\\` are escaped by writing additional `\\` 
-before them. 
+characters `0` and `\\` are escaped by writing additional `\\`
+before them.
 
 This is implmented in the function `::write_gb_string` and the
 deserialisation is implemented in `irep_serializationt::read_gb_string`.
@@ -329,18 +329,37 @@ serialisation queries save only that integer hash code of the string.
 
 \subsubsection irep-serialization-ireps Serialization of `irept` Instances
 
-
+<br>
 \subsection CProver-output CProver output - printing
-Cprover has 3 principal types of output:
+CProver has 3 types of output:
+
+* messages - filtered by a 'verbosity' level.
 
-* direct output via std::cout & std::cerr (these are in the process of being removed).
+    \ref messaget provides messages with a built-in verbosity level.
+    These are then processed by a subclass of \ref message_handlert - which
+    filters out all messages above a set verbosity level.
+    An example of this is \ref stream_message_handlert and its subtypes, which
+    directs messages to an output stream (`std::cout` & `std::cerr`, `std::clog` is not used).
+    CProver output can be in plain text, json or xml. By default the verbosity
+    filtering is set to the maximum level (10), i.e. all messages are printed
+    (level 10 messages are debug information).
+    Message level information can be found in \ref messaget.
 
 * output from invariants / exceptions
-Invariants output to std::cerr - and provide a backtrace and optionally some diagnostic information.
-For more information on invariants, see `invariant.h`
-Exceptions also print to std::cerr - and have a standard 'what()' interface. More information on exceptions can be found in `exception_utils.h`.
 
-* messages - filtered by a 'verbosity' level.
-\ref messaget provides messages with a built-in verbosity 'level'.
-These are then processed by a subclass of \ref message_handlert - which filters out all messages above a set verbosity level.  An example of this is \ref stream_message_handlert and its subtypes, which directs messages to an output stream (std::cout & std::cerr - std::log is not used).
-By default the verbosity filtering level is set to the maximum level (10) - all messages are printed (level 10 messages are debug information). Message level information can be found in \ref messaget.
+    Invariants output to `std::cerr` - and provide a backtrace and optionally
+    some diagnostic information.
+    For more information on invariants, see `invariant.h`
+    Exceptions have a standard `what()` interface. Best practice for exceptions
+    is for the output of `what()` to be routed via a message with verbosity level 1
+     (as returned by `messaget::error()`). The message is then processed by a
+     message_handler. Where plain text output (versus json or xml output) is
+     chosen,  exceptions print (indirectly) to `std::cerr`.
+     Json and xml output always goes to `std::cout`.
+     More information on exceptions can be found in `exception_utils.h`.
+
+* direct output via `std::cout` & `std::cerr`
+
+    These are in the process of being removed - no new output should go
+    via `std::cout` or `std::cerr`, but should instead use the
+    \ref messaget and \ref message_handlert infrastructure.