1\DOC HOL_ERR
2
3\BLTYPE
4HOL_ERR : {message : string, origin_function : string,
5           origin_structure : string} -> exn
6\ELTYPE
7
8\SYNOPSIS
9Standard HOL exception.
10
11\KEYWORDS
12exception, error
13
14\DESCRIBE
15{HOL_ERR} is the single exception that HOL functions are expected to raise
16when they encounter an anomalous situation.
17
18\EXAMPLE
19Building an application of {HOL_ERR} and binding it to an ML variable
20{
21   val test_exn =
22      HOL_ERR {origin_structure = "Foo",
23               origin_function = "bar",
24               message = "incomprehensible input"};
25}
26
27yields
28{
29   val test_exn = HOL_ERR : exn
30}
31
32One can scrutinize the contents of an application of {HOL_ERR} by
33pattern matching:
34{
35   - val HOL_ERR r = test_exn;
36
37   > val r = {message = "incomprehensible input",
38              origin_function = "bar",
39              origin_structure = "Foo"}
40}
41
42In current ML implementations supporting HOL, exceptions that propagate
43to the top level without being handled do not print informatively:
44{
45   - raise test_exn;
46   ! Uncaught exception:
47   ! HOL_ERR
48}
49
50In such cases, the functions {Raise} and {exn_to_string} can be used
51to obtain useful information:
52{
53   - Raise test_exn;
54
55   Exception raised at Foo.bar:
56   incomprehensible input
57   ! Uncaught exception:
58   ! HOL_ERR
59
60   - print(exn_to_string test_exn);
61
62   Exception raised at Foo.bar:
63   incomprehensible input
64   > val it = () : unit
65}
66
67
68\SEEALSO
69Feedback, Feedback.error_record, Feedback.mk_HOL_ERR, Feedback.Raise, Feedback.exn_to_string.
70\ENDDOC
71