Documentation

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.

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

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
Equations
  • s.codepointPosToUtf16Pos pos = s.codepointPosToUtf16PosFrom pos 0

Computes the position of the Unicode codepoint at UTF-16 offset utf16pos in the substring of s starting at UTF-8 offset off.

Equations

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

Computes an UTF-8 offset into text.source from an LSP-style 0-indexed (ln, col) position.

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

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 } }