Raise : exn -> 'a
STRUCTURE
Feedback
SYNOPSIS
Print an exception before re-raising it.
DESCRIPTION
The Raise function prints out information about its argument exception before re-raising it. It uses the value of ERR_to_string to format the message, and prints the information on the outstream held in ERR_outstream.
FAILURE
Never fails, since it always succeeds in raising the supplied exception.
EXAMPLE
- Raise (mk_HOL_ERR "Foo" "bar" "incomprehensible input");

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

SEEALSO
Feedback, ERR_to_string, ERR_outstream, try, trye
HOL  Trindemossen-1