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

Equations

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

def String.utf16Length (s : String) : Nat

Equations

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

def String.codepointPosToUtf16PosFrom (s : String) (n : Nat) (off : String.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

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

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

Equations

• String.codepointPosToUtf16Pos s pos = String.codepointPosToUtf16PosFrom s pos 0

def String.utf16PosToCodepointPosFrom (s : String) (utf16pos : Nat) (off : String.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

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

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

Equations

• String.utf16PosToCodepointPos s pos = String.utf16PosToCodepointPosFrom s pos 0

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

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

Equations

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

def Lean.FileMap.lspPosToUtf8Pos (text : Lean.FileMap) (pos : Lean.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 : Lean.FileMap) : Lean.Position → Lean.Lsp.Position

Equations

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

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

Equations

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

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

Gets the LSP range from a String.Range.

Equations

• Lean.FileMap.utf8RangeToLspRange text range = { start := Lean.FileMap.utf8PosToLspPos text range.start, end := Lean.FileMap.utf8PosToLspPos text range.stop }

def Lean.DeclarationRange.toLspRange (r : Lean.DeclarationRange) : Lean.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

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