HOL_MESG
Feedback.HOL_MESG : string -> unit
Prints out a message in a special format.
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.>>
See also
Feedback, Feedback.HOL_ERR,
Feedback.Raise,
Feedback.HOL_WARNING,
Feedback.MESG_to_string,
Feedback.format_MESG,
Feedback.MESG_outstream