origins_of
origins_of : hol_error -> origin list
Extract origin stack from a hol_error.
An invocation origins_of holerr returns the list of origin
elements held in holerr.
Example
> origins_of (mk_hol_error "Foo" "bar" locn.Loc_Unknown "bad input");
val it =
[{origin_function = "bar", origin_structure = "Foo",
source_location = <??>}]: origin list
Failure
Never fails.
See also
Feedback,
Feedback.mk_hol_error,
Feedback.message_of,
Feedback.top_structure_of,
Feedback.top_function_of