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