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