feat: resolve symlinks in LEAN_SRC_PATH

This commit is contained in:
Sebastian Ullrich 2021-11-16 11:51:44 +01:00
parent c5b6968c86
commit 44f9edff87

View file

@ -69,8 +69,12 @@ partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
let mod? ← findModuleOf? n
let modUri? ← match mod? with
| some modName =>
let modFname? ← rc.srcSearchPath.findWithExt "lean" modName
pure <| modFname?.map toFileUri
let some modFname ← rc.srcSearchPath.findWithExt "lean" modName
| pure none
-- resolve symlinks (such as `src` in the build dir) so that files are opened
-- in the right folder
let modFname ← IO.FS.realPath modFname
pure <| some <| toFileUri modFname
| none => pure <| some doc.meta.uri
let ranges? ← findDeclarationRanges? n