Skip to content

Commit

Permalink
fix: handle unimported builtin names for location links (#4780)
Browse files Browse the repository at this point in the history
The function `locationLinksFromDecl` could throw an error if the name it
is provided doesn't exist in the environment, which is possible if for
example an elaborator is a builtin.

Closes #3789
  • Loading branch information
kmill authored Jul 27, 2024
1 parent 10f5f43 commit 30c78a4
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions src/Lean/Server/GoTo.lean
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,8 @@ def moduleFromDocumentUri (srcSearchPath : SearchPath) (uri : DocumentUri)
open Elab in
def locationLinksFromDecl (srcSearchPath : SearchPath) (uri : DocumentUri) (n : Name)
(originRange? : Option Range) : MetaM (Array LocationLink) := do
-- Potentially this name is a builtin that has not been imported yet:
unless (← getEnv).contains n do return #[]
let mod? ← findModuleOf? n
let modUri? ← match mod? with
| some modName => documentUriFromModule srcSearchPath modName
Expand Down

0 comments on commit 30c78a4

Please sign in to comment.