top_structure_of
top_structure_of : hol_error -> string
Extract last structure name added to a hol_error.
An invocation top_structure_of holerr returns the structure name of
the top origin element held in holerr.
Example
> top_structure_of
(mk_hol_error "Foo" "bar" locn.Loc_Unknown "bad input")
val it = "Foo": string
Failure
The call fails if the origin stack of the hol_error is empty.
See also
Feedback,
Feedback.mk_hol_error,
Feedback.origins_of,
Feedback.message_of,
Feedback.top_function_of,
Feedback.top_location_of,
Feedback.set_top_structure