Raise
Feedback.Raise : exn -> 'a
Print an exception before re-raising it.
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- The type of (it) contains a free type variable. Setting it to a unique
monotype.
Exception raised at Foo.bar: incomprehensible input
HOL_ERR (at Foo.bar: incomprehensible input) raised
See also
Feedback,
Feedback.ERR_to_string,
Feedback.ERR_outstream,
Lib.try, Lib.trye