exn_to_string

Feedback.exn_to_string : exn -> string

Map an exception into a string.

The function exn_to_string maps an exception to a string. However, in the case of the Interrupt exception, it is not mapped to a string, but is instead raised. This avoids the possibility of suppressing the propagation of Interrupt to the top level.

Failure

Never fails.

Example

> exn_to_string Interrupt;
Exception- Interrupt raised

> exn_to_string Div;
val it = "Div": string

> exn_to_string (mk_HOL_ERR "Foo" "bar" "incomprehensible input");
val it = "\nException raised at Foo.bar: incomprehensible input\n": string

See also

Feedback, Feedback.HOL_ERR, Feedback.ERR_to_string