format_MESG
Feedback.format_MESG : string -> string
Maps argument of HOL_MESG to a string.
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
> format_MESG "Hello world.";
val it = "<<HOL message: Hello world.>>\n": string
See also
Feedback,
Feedback.MESG_to_string,
Feedback.format_ERR,
Feedback.format_WARNING