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