WARNING_to_string : (string -> string -> string -> string) ref
STRUCTURE
Feedback
SYNOPSIS
Alterable function for formatting HOL_WARNING.
DESCRIPTION
WARNING_to_string is a reference to a function for formatting the argument to HOL_WARNING.

The default value of WARNING_to_string is format_WARNING.

EXAMPLE
    - fun alt_WARNING_report s t u =
        String.concat["WARNING---", s,".",t,": ",u,"---END WARNING\n"];

    - WARNING_to_string := alt_WARNING_report;

    - HOL_WARNING "Foo" "bar" "Look out";
    WARNING---Foo.bar: Look out---END WARNING
    > val it = () : unit

SEEALSO
Feedback, HOL_WARNING, format_WARNING, ERR_to_string, MESG_to_string
HOL  Kananaskis-13