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