\DOC exn_to_string

\TYPE {exn_to_string : exn -> string}

\SYNOPSIS
Map an exception into a string.

\KEYWORDS
exception, formatting

\DESCRIBE
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, Feedback.HOL_ERR, Feedback.ERR_to_string.
\ENDDOC