LSP uses UTF-16 for indexing, so we need to provide some primitives to interact with Lean strings using UTF-16 indices.

def Char.utf16Size (c : Char) : UInt32

Returns the number of bytes required to encode this Char in UTF-16.

def String.utf16Length (s : String) : Nat

def String.codepointPosToUtf16PosFrom (s : String) (n : Nat) (off : Pos) : Nat

Computes the UTF-16 offset of the n-th Unicode codepoint in the substring of s starting at UTF-8 offset off. Yes, this is actually useful.

def String.codepointPosToUtf16Pos (s : String) (pos : Nat) : Nat

def String.utf16PosToCodepointPosFrom (s : String) (utf16pos : Nat) (off : Pos) : Nat

Computes the position of the Unicode codepoint at UTF-16 offset utf16pos in the substring of s starting at UTF-8 offset off.

def String.utf16PosToCodepointPos (s : String) (pos : Nat) : Nat

def String.codepointPosToUtf8PosFrom (s : String) : Pos → Nat → Pos

Starting at utf8pos, finds the UTF-8 offset of the p-th codepoint.

def Lean.FileMap.lspPosToUtf8Pos (text : FileMap) (pos : Lsp.Position) : String.Pos

Computes an UTF-8 offset into text.source from an LSP-style 0-indexed (ln, col) position.

def Lean.FileMap.leanPosToLspPos (text : FileMap) : Position → Lsp.Position

def Lean.FileMap.utf8PosToLspPos (text : FileMap) (pos : String.Pos) : Lsp.Position

def Lean.FileMap.utf8RangeToLspRange (text : FileMap) (range : String.Range) : Lsp.Range

Gets the LSP range from a String.Range.

def Lean.FileMap.lspRangeToUtf8Range (text : FileMap) (range : Lsp.Range) : String.Range

def Lean.DeclarationRange.ofFilePositions (text : FileMap) (pos endPos : Position) : DeclarationRange

def Lean.DeclarationRange.ofStringPositions (text : FileMap) (pos endPos : String.Pos) : DeclarationRange

def Lean.DeclarationRange.toLspRange (r : DeclarationRange) : Lsp.Range

Convert the Lean DeclarationRange to an LSP Range by turning the 1-indexed line numbering into a 0-indexed line numbering and converting the character offset within the line to a UTF-16 indexed offset.