emit_ERR
Feedback.emit_ERR : bool ref
Flag controlling output of HOL_ERR exceptions.
The boolean flag emit_ERR tells whether an application of HOL_ERR
should be printed. Its value is consulted by Raise when it attempts to
print a textual representation of its argument exception. This flag is
not commonly used, and it may disappear or change in the future.
The default value of emit_ERR is true.
Example
> Raise (mk_HOL_ERR "Module" "function" "message");
Exception- The type of (it) contains a free type variable. Setting it to a unique
monotype.
Exception raised at Module.function: message
HOL_ERR (at Module.function: message) raised
> emit_ERR := false;
val it = (): unit
> Raise (mk_HOL_ERR "Module" "function" "message");
Exception- The type of (it) contains a free type variable. Setting it to a unique
monotype.
HOL_ERR (at Module.function: message) raised
See also
Feedback, Feedback.Raise,
Feedback.emit_MESG,
Feedback.emit_WARNING