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