HOL_MESG : string -> unit
STRUCTURE
Feedback
SYNOPSIS
Prints out a message in a special format.
DESCRIPTION
HOL_MESG prints out its argument after formatting it a bit. The formatting is controlled by the function held in MESG_to_string, which is format_MESG by default. The output stream that the message is printed on is controlled by MESG_outstream, and is TextIO.stdOut by default.

There are three kinds of informative messages that the Feedback structure supports: errors, warnings, and messages. Errors are signalled by the raising of an exception built from HOL_ERR; warnings, which are printed by HOL_WARNING, are less severe than errors, and lead to a warning message being printed; finally, messages have no pejorative weight at all, and may be freely employed, via HOL_MESG, to keep users informed in the normal course of processing.

FAILURE
The invocation fails if the formatting or output routines fail.
EXAMPLE
    - HOL_MESG "Ack.";
    <<HOL message: Ack.>>

SEEALSO
Feedback, HOL_ERR, Raise, HOL_WARNING, MESG_to_string, format_MESG, MESG_outstream
HOL  Kananaskis-14