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