exn_to_string : exn -> string
STRUCTURE
Feedback
SYNOPSIS
Map an exception into a string.
DESCRIPTION
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;
> Interrupted.

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

- print
   (exn_to_string (mk_HOL_ERR "Foo" "bar" "incomprehensible input"));

Exception raised at Foo.bar:
incomprehensible input
> val it = () : unit

SEEALSO
Feedback, HOL_ERR, ERR_to_string
HOL  Kananaskis-14