format_WARNING
Feedback.format_WARNING : string -> string -> string -> string
Maps arguments of HOL_WARNING to a string.
The format_WARNING function maps three strings to a string. Usually,
the input strings are the arguments to an invocation of HOL_WARNING.
format_WARNING is the default function used by WARNING_to_string.
Failure
Never fails.
Example
> format_WARNING "Module" "function" "Gadzooks!";
val it = "<<HOL warning: Module.function: Gadzooks!>>\n": string
See also
Feedback,
Feedback.WARNING_to_string,
Feedback.format_ERR,
Feedback.format_MESG