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

def Lean.Char.utf16Size (c : Char) : UInt32

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

def Lean.String.utf16Length (s : String) : Nat

def Lean.String.codepointPosToUtf16PosFrom (s : String) (n : Nat) (off : String.Pos.Raw) : 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 Lean.String.codepointPosToUtf16Pos (s : String) (pos : Nat) : Nat

def Lean.String.utf16PosToCodepointPosFrom (s : String) (utf16pos : Nat) (off : String.Pos.Raw) : 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 Lean.String.utf16PosToCodepointPos (s : String) (pos : Nat) : Nat

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

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

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

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.Raw) : Lsp.Position

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

Gets the LSP range from a Lean.Syntax.Range.

def Lean.FileMap.lspRangeOfStx? (text : FileMap) (stx : Syntax) (canonicalOnly : Bool := false) : Option Lsp.Range

Gets the LSP range of syntax stx.

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

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

def Lean.DeclarationRange.ofStringPositions (text : FileMap) (pos endPos : String.Pos.Raw) : 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.