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

def String.utf16Length (s : String) : Nat

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.

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

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.

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

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.

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

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