Documentation

Lean.Data.Lsp.Utf16

def Char.utf16Size (c : Char) :

Equations

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

def String.utf16Length (s : String) :

Equations

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

def String.codepointPosToUtf16PosFrom (s : String) (n : Nat) (off : String.Pos) :

Equations

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

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

Equations

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

def String.utf16PosToCodepointPosFrom (s : String) (utf16pos : Nat) (off : String.Pos) :

Equations

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

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

Equations

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

def String.codepointPosToUtf8PosFrom (s : String) :

String.Pos → Nat → String.Pos

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) :

Equations

Lean.FileMap.lspPosToUtf8Pos text pos = let colPos := if h : pos.line < Array.size text.positions then Array.get text.positions { val := pos.line, isLt := h } else if Array.isEmpty text.positions = true then 0 else Array.back text.positions; let chr := String.utf16PosToCodepointPosFrom text.source pos.character colPos; String.codepointPosToUtf8PosFrom text.source colPos chr

def Lean.FileMap.leanPosToLspPos (text : Lean.FileMap) :

Lean.Position → Lean.Lsp.Position

Equations

Lean.FileMap.leanPosToLspPos text x = match x with | { line := ln, column := col } => { line := ln - 1, character := String.codepointPosToUtf16PosFrom text.source col (Array.get! text.positions (ln - 1)) }

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)