emit_MESG
Feedback.emit_MESG : bool ref
Flag controlling output of HOL_MESG function.
The boolean flag emit_MESG is consulted by HOL_MESG 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_MESG is true.
Example
> HOL_MESG "Joy to the world.";
<<HOL message: Joy to the world.>>
val it = (): unit
> emit_MESG := false;
val it = (): unit
> HOL_MESG "Peace on Earth.";
val it = (): unit
See also
Feedback, Feedback.HOL_MESG,
Feedback.emit_ERR,
Feedback.emit_WARNING