emit_WARNING

Feedback.emit_WARNING : bool ref

Flag controlling output of HOL_WARNING function.

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

See also

Feedback, Feedback.HOL_WARNING, Feedback.emit_ERR, Feedback.emit_MESG