rzk-0.11.3: An experimental proof assistant for synthetic ∞-categories
Safe HaskellNone
LanguageHaskell2010

Language.Rzk.VSCode.PositionEncoding

Description

Conversion between code-point and UTF-16 positions at the LSP boundary.

LSP positions count UTF-16 code units (the default position encoding, and the only one VS Code supports), while alex positions and everything derived from them (the surface AST, the reference index, the typechecker) count Unicode code points. The two agree except on lines containing astral-plane characters (code points above U+FFFF, such as 𝕀), each of which takes two UTF-16 units. Emitting a code-point column for such a line shifts every position to the right of the character, and a range boundary can land in the middle of a surrogate pair, which is what shatters the glyph in the editor (see issue #303).

Everything internal stays in code points; the handlers convert with this module when crossing the wire, in both directions. AstralLines records only the lines where the two encodings differ, so for the common all-BMP document every conversion is an identity after one map lookup.

Synopsis

Documentation

data AstralLines Source #

The lines of a document on which code-point and UTF-16 columns differ, keyed by 0-based line number.

utf16Length :: Text -> Int Source #

The length of a text in UTF-16 code units.

colToUtf16 :: AstralLines -> Int -> Int -> Int Source #

Convert a 0-based code-point column on the given 0-based line to UTF-16 units. A column beyond the end of the line keeps its distance past the end (the diagnostics code uses column 99 to mean "to the end of the line").

colFromUtf16 :: AstralLines -> Int -> Int -> Int Source #

Convert a 0-based UTF-16 column on the given 0-based line to code points. A column inside a surrogate pair maps to the start of its character.

positionFromUtf16 :: AstralLines -> Position -> Position Source #

Convert an incoming LSP position (UTF-16) to code points.

rangeToUtf16 :: AstralLines -> Range -> Range Source #

Convert an outgoing range (code points) to UTF-16.

tokensToUtf16 :: AstralLines -> [SemanticTokenAbsolute] -> [SemanticTokenAbsolute] Source #

Convert semantic tokens (code points) to UTF-16. The length is converted through the token's end column, so a token that itself contains astral characters (e.g. the 𝕀 keyword) gets its UTF-16 width.