emit_WARNING : bool ref
STRUCTURE
Feedback
SYNOPSIS
Flag controlling output of HOL_WARNING function.
DESCRIPTION
The boolean flag emit_WARNING is consulted by HOL_WARNING when it attempts to print its argument. This flag is not commonly used, and it may disappear or change in the future.

The default value of emit_WARNING is true.

EXAMPLE
- HOL_WARNING "Clock" "watcher" "Time is running out.";
<<HOL warning: Clock.watcher: Time is running out.>>
> val it = () : unit

- emit_WARNING := false;
> val it = () : unit

- HOL_WARNING "Clock" "watcher" "Time is running out.";
> val it = () : unit

SEEALSO
Feedback, HOL_WARNING, emit_ERR, emit_MESG
HOL  Kananaskis-14