top_location_of

   top_location_of : hol_error -> locn.locn

Extract last location added to a hol_error.

An invocation top_location_of holerr returns the location of the top origin element held in holerr.

Example

   > val exloc = let open locn in Loc (LocA(0,0), LocA(3,42)) end;
   val exloc = 1:0-4:42: locn.locn

   > top_location_of (mk_hol_error "Foo" "bar" exloc "bad input");
   val it = 1:0-4:42: locn.locn

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_structure_of, Feedback.top_function_of