Feedback.HOL

Building an application of HOL_ERR and binding it to an ML variable

   val test_exn =
      HOL_ERR {origin_structure = "Foo",
               origin_function = "bar",
               message = "incomprehensible input"};

yields

   val test_exn = HOL_ERR : exn

One can scrutinize the contents of an application of HOL_ERR by pattern matching:

   - val HOL_ERR r = test_exn;

   > val r = {message = "incomprehensible input",
              origin_function = "bar",
              origin_structure = "Foo"}

In current ML implementations supporting HOL, exceptions that propagate to the top level without being handled do not print informatively:

   - raise test_exn;
   ! Uncaught exception:
   ! HOL_ERR

In such cases, the functions Raise and exn_to_string can be used to obtain useful information:

   - Raise test_exn;

   Exception raised at Foo.bar:
   incomprehensible input
   ! Uncaught exception:
   ! HOL_ERR

   - print(exn_to_string test_exn);

   Exception raised at Foo.bar:
   incomprehensible input
   > val it = () : unit