1\DOC exn_to_string
2
3\TYPE {exn_to_string : exn -> string}
4
5\SYNOPSIS
6Map an exception into a string.
7
8\KEYWORDS
9exception, formatting
10
11\DESCRIBE
12The function {exn_to_string} maps an exception to a string. However,
13in the case of the {Interrupt} exception, it is not mapped to a
14string, but is instead raised. This avoids the possibility of
15suppressing the propagation of {Interrupt} to the top level.
16
17\FAILURE
18Never fails.
19
20\EXAMPLE
21{
22- exn_to_string Interrupt;
23> Interrupted.
24
25- exn_to_string Div;
26> val it = "Div" : string
27
28- print
29   (exn_to_string (mk_HOL_ERR "Foo" "bar" "incomprehensible input"));
30
31Exception raised at Foo.bar:
32incomprehensible input
33> val it = () : unit
34}
35
36
37\SEEALSO
38Feedback, Feedback.HOL_ERR, Feedback.ERR_to_string.
39\ENDDOC
40