----------------------------------------------------------------------
format_MESG                                                 (Feedback)
----------------------------------------------------------------------
format_MESG : string -> string

SYNOPSIS
Maps argument of {HOL_MESG} to a string.

KEYWORDS
message, formatting

DESCRIBE
The {format_MESG} function maps a string to a string. Usually, the input
string is the argument of an invocation of {HOL_MESG}. {format_MESG} is
the default function used by {MESG_to_string}.

FAILURE
Never fails.

EXAMPLE

- print (format_MESG "Hello world.");
<<HOL message: Hello world.>>




SEEALSO
Feedback, Feedback.MESG_to_string, Feedback.format_ERR,
Feedback.format_WARNING.

----------------------------------------------------------------------