diff --git a/src/Lean/DeclarationRange.lean b/src/Lean/DeclarationRange.lean index 81078f8955..4d8e4e5e4c 100644 --- a/src/Lean/DeclarationRange.lean +++ b/src/Lean/DeclarationRange.lean @@ -9,8 +9,15 @@ import Lean.AuxRecursor namespace Lean structure DeclarationRange where - pos : Position - endPos : Position + pos : Position + /-- A precomputed UTF-16 `character` field as in `Lean.Lsp.Position`. We need to store this + because LSP clients want us to report the range in terms of UTF-16, but converting a Unicode + codepoint stored in `Lean.Position` to UTF-16 requires loading and mapping the target source + file, which is IO-heavy. -/ + charUtf16 : Nat + endPos : Position + /-- See `charUtf16`. -/ + endCharUtf16 : Nat deriving Inhabited, DecidableEq, Repr structure DeclarationRanges where diff --git a/src/Lean/Elab/DeclarationRange.lean b/src/Lean/Elab/DeclarationRange.lean index 2786371f42..8b6d33c772 100644 --- a/src/Lean/Elab/DeclarationRange.lean +++ b/src/Lean/Elab/DeclarationRange.lean @@ -5,14 +5,21 @@ Authors: Leonardo de Moura -/ import Lean.DeclarationRange import Lean.Elab.Log +import Lean.Data.Lsp.Utf16 namespace Lean.Elab def getDeclarationRange [Monad m] [MonadFileMap m] (stx : Syntax) : m DeclarationRange := do - let pos := stx.getPos.getD 0 - let endPos := stx.getTailPos.getD pos let fileMap ← getFileMap - return { pos := fileMap.toPosition pos, endPos := fileMap.toPosition endPos } + let pos := stx.getPos.getD 0 + let endPos := stx.getTailPos.getD pos |> fileMap.toPosition + let pos := pos |> fileMap.toPosition + return { + pos := pos + charUtf16 := fileMap.leanPosToLspPos pos |>.character + endPos := endPos + endCharUtf16 := fileMap.leanPosToLspPos endPos |>.character + } /-- For most builtin declarations, the selection range is just its name, which is stored in the second position. diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 3547f90766..2d1f8c6438 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -414,13 +414,14 @@ section RequestHandling let ranges? ← ci.runMetaM i.lctx <| findDeclarationRanges? n if let (some ranges, some mod) := (ranges?, mod?) then - let rangeToLspRange (r : DeclarationRange) : Lsp.Range := - ⟨text.leanPosToLspPos r.pos, text.leanPosToLspPos r.endPos⟩ + let declRangeToLspRange (r : DeclarationRange) : Lsp.Range := + { start := ⟨r.pos.line - 1, r.charUtf16⟩ + «end» := ⟨r.endPos.line - 1, r.endCharUtf16⟩ } let ll : LocationLink := { originSelectionRange? := some ⟨text.utf8PosToLspPos i.pos?.get!, text.utf8PosToLspPos i.tailPos?.get!⟩ targetUri := mod - targetRange := rangeToLspRange ranges.range - targetSelectionRange := rangeToLspRange ranges.selectionRange + targetRange := declRangeToLspRange ranges.range + targetSelectionRange := declRangeToLspRange ranges.selectionRange } return #[ll] return #[]