diff options
| author | Emilio Jesus Gallego Arias | 2020-02-11 11:33:55 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-15 02:19:01 +0200 |
| commit | 7e078b070b3acf6c0b24d66a150b09a7df57b09d (patch) | |
| tree | 380d22bee9648f4b828141f035500d9d2cd3ad04 /library | |
| parent | 56e23844e80e6d607ad5fa56dfeedcd70e97ee70 (diff) | |
[misc] Better preserve backtraces in several modules
Re-raising inside exception handlers must be done with care in order
to preserve backtraces; even if newer OCaml versions do a better job
in automatically spilling `%reraise` in places that matter, there is
no guarantee for that to happen.
I've done a best-effort pass of places that were re-raising
incorrectly, hopefully I got the logic right.
There is the special case of `Nametab.error_global_not_found` which is
raised many times in response to a `Not_found` error; IMHO this error
should be converted to something more specific, however the scope of
that change would be huge as to do easily...
Diffstat (limited to 'library')
| -rw-r--r-- | library/nametab.ml | 16 | ||||
| -rw-r--r-- | library/nametab.mli | 2 |
2 files changed, 11 insertions, 7 deletions
diff --git a/library/nametab.ml b/library/nametab.ml index d9b4dc9122..a51c281f2b 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -43,8 +43,9 @@ end exception GlobalizationError of qualid -let error_global_not_found qid = - Loc.raise ?loc:qid.CAst.loc (GlobalizationError qid) +let error_global_not_found ~info qid = + let info = Option.cata (Loc.add_loc info) info qid.CAst.loc in + Exninfo.iraise (GlobalizationError qid, info) (* The visibility can be registered either - for all suffixes not shorter then a given int - when the object @@ -499,8 +500,9 @@ let global qid = user_err ?loc:qid.CAst.loc ~hdr:"global" (str "Unexpected reference to a notation: " ++ pr_qualid qid) - with Not_found -> - error_global_not_found qid + with Not_found as exn -> + let _, info = Exninfo.capture exn in + error_global_not_found ~info qid (* Exists functions ********************************************************) @@ -566,8 +568,10 @@ let shortest_qualid_of_universe ?loc kn = let pr_global_env env ref = try pr_qualid (shortest_qualid_of_global env ref) - with Not_found as e -> - if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e + with Not_found as exn -> + let exn, info = Exninfo.capture exn in + if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); + Exninfo.iraise (exn, info) let global_inductive qid = let open GlobRef in diff --git a/library/nametab.mli b/library/nametab.mli index 00cec35506..8a8b59733c 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -91,7 +91,7 @@ end exception GlobalizationError of qualid (** Raises a globalization error *) -val error_global_not_found : qualid -> 'a +val error_global_not_found : info:Exninfo.info -> qualid -> 'a (** {6 Register visibility of things } *) |