Lean.Data.Lsp.Utf16

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

source

def Char.utf16Size (c : Char) :

UInt32

Equations

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

source

def String.utf16Length (s : String) :

Nat

Equations

String.utf16Length s = String.foldr (fun c acc => String.csize16 c + acc) 0 s

source

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

source

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

Nat

Equations

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

source

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

source

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

Nat

Equations

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

source

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 _fun_discr 0 = _fun_discr
String.codepointPosToUtf8PosFrom s _fun_discr (Nat.succ p) = String.codepointPosToUtf8PosFrom s (String.next s _fun_discr) p

source

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.

source

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.

source

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)