render_exn
Feedback.render_exn : exn -> 'a
Print HOL_ERR exception then recover, or not, according to
Globals.interactive.
The variable Globals.interactive is used by programs to tell whether
the HOL4 system is running interactively (i.e. is in the
Read-Eval-Print loop) or not (is running in batch mode under
Holmake). When the contents of Globals.interactive is true
render_exn raises the given exception. If the exception is not
otherwise dealt with in user code, the REPL will handle it and print
the message contents before resuming the top-level loop.
When the contents of Globals.interactive is false, render_exn
prints a message derived from the contents of its argument exception
then exits to the host operating system.
Example
> val () = render_exn (mk_HOL_ERR "S" "f" "-");
Exception- HOL_ERR (at S.f: -) raised
> Globals.interactive := false; (* for example purposes only! *)
val it = (): unit
> val () = render_exn (mk_HOL_ERR "S" "f" "-");
Exception raised at S.f: -
Process HOL exited abnormally with code 1
Comment
render_exn attempts to display non-HOL_ERR exceptions sensibly.