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.

Equations

• c.utf16Size = if c.val ≤ 65535 then 1 else 2

def String.utf16Length (s : String) : Nat

Equations

• s.utf16Length = String.foldr (fun (c : Char) (acc : Nat) => String.csize16✝ c + acc) 0 s

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.

Equations

• s.codepointPosToUtf16PosFrom n off = String.codepointPosToUtf16PosFromAux✝ s n off 0

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

Equations

• s.codepointPosToUtf16Pos pos = s.codepointPosToUtf16PosFrom pos 0

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.

Equations

• s.utf16PosToCodepointPosFrom utf16pos off = String.utf16PosToCodepointPosFromAux✝ s utf16pos off 0

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

Equations

• s.utf16PosToCodepointPos pos = s.utf16PosToCodepointPosFrom pos 0

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

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

Equations

• s.codepointPosToUtf8PosFrom x✝ 0 = x✝
• s.codepointPosToUtf8PosFrom x✝ p.succ = s.codepointPosToUtf8PosFrom (s.next x✝) p

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• text.leanPosToLspPos { line := line, column := col } = { line := line - 1, character := text.source.codepointPosToUtf16PosFrom col (Lean.FileMap.lineStartPos✝ text (line - 1)) }

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

Equations

• text.utf8PosToLspPos pos = text.leanPosToLspPos (text.toPosition pos)

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

Gets the LSP range from a String.Range.

Equations

• text.utf8RangeToLspRange range = { start := text.utf8PosToLspPos range.start, «end» := text.utf8PosToLspPos range.stop }

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

Equations

• text.lspRangeToUtf8Range range = { start := text.lspPosToUtf8Pos range.start, stop := text.lspPosToUtf8Pos range.end }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.DeclarationRange.ofStringPositions text pos endPos = Lean.DeclarationRange.ofFilePositions text (text.toPosition pos) (text.toPosition endPos)

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.

Equations

• r.toLspRange = { start := { line := r.pos.line - 1, character := r.charUtf16 }, «end» := { line := r.endPos.line - 1, character := r.endCharUtf16 } }