Skip to content

Commit

Permalink
Merge pull request #739 from coq-community/lib-error-loc
Browse files Browse the repository at this point in the history
Capture the correct loc for when an import fails.
  • Loading branch information
rtetley authored Feb 20, 2024
2 parents 1851e28 + 069270b commit 367317b
Showing 1 changed file with 15 additions and 1 deletion.
16 changes: 15 additions & 1 deletion language-server/dm/document.ml
Original file line number Diff line number Diff line change
Expand Up @@ -302,6 +302,20 @@ exception E = Stream.Error
exception E = Grammar.Error
[%%endif]

[%%if coq = "8.18" || coq = "8.19"]
let get_loc_from_info_or_exn exn =
let e, info = Exninfo.capture exn in
match e with
| Synterp.UnmappedLibrary (_, qid) -> qid.loc
| Synterp.NotFoundLibrary (_, qid) -> qid.loc
| _ -> Loc.get_loc @@ info
[%%else]
let get_loc_from_info_or_exn exn =
let _, info = Exninfo.capture exn in
Loc.get_loc @@ info
[%%endif]


let rec parse_more synterp_state stream raw parsed errors =
let handle_parse_error start msg =
log @@ "handling parse error at " ^ string_of_int start;
Expand Down Expand Up @@ -338,7 +352,7 @@ let rec parse_more synterp_state stream raw parsed errors =
parse_more synterp_state stream raw parsed errors
with exn ->
let e, info = Exninfo.capture exn in
let loc = Loc.get_loc @@ info in
let loc = get_loc_from_info_or_exn exn in
handle_parse_error start (loc, Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info))
end
| exception (E msg as exn) ->
Expand Down

0 comments on commit 367317b

Please sign in to comment.