diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml index 12ebe4ff3..8cff6e38b 100644 --- a/language-server/dm/document.ml +++ b/language-server/dm/document.ml @@ -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; @@ -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) ->