Lapis.Server.SemanticTokens

source

def Lapis.Server.SemanticTokens.standardTokenTypes :

Array String

Standard semantic token types as defined by LSP 3.17

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Lapis.Server.SemanticTokens.standardTokenModifiers :

Array String

Standard semantic token modifiers as defined by LSP 3.17

Equations

Lapis.Server.SemanticTokens.standardTokenModifiers = #["declaration", "definition", "readonly", "static", "deprecated", "abstract", "async", "modification", "documentation", "defaultLibrary"]

Instances For

source

def Lapis.Server.SemanticTokens.tokenTypeIndex (tokenType : Protocol.Generated.SemanticTokenTypes) :

Nat

Get the index of a token type in the standard list

Equations

Instances For

source

def Lapis.Server.SemanticTokens.tokenModifierBit (modifier : Protocol.Generated.SemanticTokenModifiers) :

Nat

Get the bit position of a token modifier in the standard list

Equations

Instances For

source

def Lapis.Server.SemanticTokens.encodeModifiers (modifiers : Array Protocol.Generated.SemanticTokenModifiers) :

Nat

Encode multiple modifiers as a bitmask

Equations

One or more equations did not get rendered due to their size.

Instances For

source

structure Lapis.Server.SemanticTokens.Token :

Type

A semantic token before encoding. Tokens are represented with absolute positions and will be converted to relative (delta) encoding when building the response.

line : Nat
Line number (0-indexed)
character : Nat
Character offset within the line (0-indexed, UTF-16 code units)
length : Nat
Length of the token in UTF-16 code units
tokenType : Nat
Index into the token types legend
tokenModifiers : Nat
Bitmask of token modifiers

Instances For

source

def Lapis.Server.SemanticTokens.instInhabitedToken.default :

Token

Equations

Lapis.Server.SemanticTokens.instInhabitedToken.default = { line := default, character := default, length := default, tokenType := default, tokenModifiers := default }

Instances For

source

instance Lapis.Server.SemanticTokens.instInhabitedToken :

Inhabited Token

Equations

Lapis.Server.SemanticTokens.instInhabitedToken = { default := Lapis.Server.SemanticTokens.instInhabitedToken.default }

source

def Lapis.Server.SemanticTokens.instReprToken.repr :

Token → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.

Instances For

source

instance Lapis.Server.SemanticTokens.instReprToken :

Repr Token

Equations

Lapis.Server.SemanticTokens.instReprToken = { reprPrec := Lapis.Server.SemanticTokens.instReprToken.repr }

source

def Lapis.Server.SemanticTokens.instBEqToken.beq :

Token → Token → Bool

Equations

One or more equations did not get rendered due to their size.
Lapis.Server.SemanticTokens.instBEqToken.beq x✝¹ x✝ = false

Instances For

source

instance Lapis.Server.SemanticTokens.instBEqToken :

BEq Token

Equations

Lapis.Server.SemanticTokens.instBEqToken = { beq := Lapis.Server.SemanticTokens.instBEqToken.beq }

source

def Lapis.Server.SemanticTokens.Token.ofType (line character length : Nat) (tokenType : Protocol.Generated.SemanticTokenTypes) (modifiers : Array Protocol.Generated.SemanticTokenModifiers := #[]) :

Token

Create a token from a SemanticTokenTypes enum

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Lapis.Server.SemanticTokens.Token.ofTypeIndex (line character length typeIndex : Nat) (modifierBits : Nat := 0) :

Token

Create a token with a custom type index

Equations

One or more equations did not get rendered due to their size.

Instances For

source

structure Lapis.Server.SemanticTokens.TokenBuilder :

Type

Builder for collecting tokens before encoding

tokens : Array Token
Collected tokens (unsorted)
tokenTypes : Array String
Token types legend
tokenModifiers : Array String
Token modifiers legend

Instances For

source

def Lapis.Server.SemanticTokens.TokenBuilder.new :

TokenBuilder

Create a new token builder with standard legends

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Lapis.Server.SemanticTokens.TokenBuilder.withLegends (tokenTypes tokenModifiers : Array String) :

TokenBuilder

Create a token builder with custom legends

Equations

Lapis.Server.SemanticTokens.TokenBuilder.withLegends tokenTypes tokenModifiers = { tokens := #[], tokenTypes := tokenTypes, tokenModifiers := tokenModifiers }

Instances For

source

def Lapis.Server.SemanticTokens.TokenBuilder.push (b : TokenBuilder) (line character length : Nat) (tokenType : Protocol.Generated.SemanticTokenTypes) (modifiers : Array Protocol.Generated.SemanticTokenModifiers := #[]) :

TokenBuilder

Add a token using the SemanticTokenTypes enum

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Lapis.Server.SemanticTokens.TokenBuilder.pushRaw (b : TokenBuilder) (line character length typeIndex : Nat) (modifierBits : Nat := 0) :

TokenBuilder

Add a token using a custom type index

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Lapis.Server.SemanticTokens.TokenBuilder.pushToken (b : TokenBuilder) (token : Token) :

TokenBuilder

Add a pre-constructed token

Equations

b.pushToken token = { tokens := b.tokens.push token, tokenTypes := b.tokenTypes, tokenModifiers := b.tokenModifiers }

Instances For

source

def Lapis.Server.SemanticTokens.TokenBuilder.pushTokens (b : TokenBuilder) (tokens : Array Token) :

TokenBuilder

Add multiple tokens

Equations

b.pushTokens tokens = { tokens := b.tokens ++ tokens, tokenTypes := b.tokenTypes, tokenModifiers := b.tokenModifiers }

Instances For

source

def Lapis.Server.SemanticTokens.TokenBuilder.getLegend (b : TokenBuilder) :

Protocol.Generated.SemanticTokensLegend

Get the legend for capability registration

Equations

b.getLegend = { tokenTypes := b.tokenTypes, tokenModifiers := b.tokenModifiers }

Instances For

source

def Lapis.Server.SemanticTokens.TokenBuilder.sortTokens (tokens : Array Token) :

Array Token

Sort tokens by position (required before encoding)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Lapis.Server.SemanticTokens.TokenBuilder.encode (b : TokenBuilder) :

Array Nat

Encode tokens to the LSP delta format. The LSP semantic tokens format uses relative encoding:

Each token is represented as 5 integers
[deltaLine, deltaStartChar, length, tokenType, tokenModifiers]
deltaLine: line offset from previous token (or from line 0 for first token)
deltaStartChar: character offset from previous token's start on same line, or from character 0 if on a different line

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Lapis.Server.SemanticTokens.TokenBuilder.build (b : TokenBuilder) (resultId : Option String := none) :

Protocol.Generated.SemanticTokens

Build the SemanticTokens response

Equations

b.build resultId = { resultId := resultId, data := b.encode }

Instances For

source

def Lapis.Server.SemanticTokens.TokenBuilder.isEmpty (b : TokenBuilder) :

Bool

Check if the builder has any tokens

Equations

b.isEmpty = b.tokens.isEmpty

Instances For

source

def Lapis.Server.SemanticTokens.TokenBuilder.size (b : TokenBuilder) :

Nat

Get the number of tokens

Equations

b.size = b.tokens.size

Instances For

source

structure Lapis.Server.SemanticTokens.OptionsBuilder :

Type

Builder for creating SemanticTokensOptions

tokenTypes : Array String
tokenModifiers : Array String
full : Bool
fullDelta : Bool
range : Bool

Instances For

source

def Lapis.Server.SemanticTokens.OptionsBuilder.new :

OptionsBuilder

Create a new options builder with standard legends

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Lapis.Server.SemanticTokens.OptionsBuilder.withTokenTypes (b : OptionsBuilder) (types : Array String) :

OptionsBuilder

Use custom token types

Equations

b.withTokenTypes types = { tokenTypes := types, tokenModifiers := b.tokenModifiers, full := b.full, fullDelta := b.fullDelta, range := b.range }

Instances For

source

def Lapis.Server.SemanticTokens.OptionsBuilder.withTokenModifiers (b : OptionsBuilder) (modifiers : Array String) :

OptionsBuilder

Use custom token modifiers

Equations

b.withTokenModifiers modifiers = { tokenTypes := b.tokenTypes, tokenModifiers := modifiers, full := b.full, fullDelta := b.fullDelta, range := b.range }

Instances For

source

def Lapis.Server.SemanticTokens.OptionsBuilder.addTokenTypes (b : OptionsBuilder) (types : Array String) :

OptionsBuilder

Add custom token types to the standard list

Equations

b.addTokenTypes types = { tokenTypes := b.tokenTypes ++ types, tokenModifiers := b.tokenModifiers, full := b.full, fullDelta := b.fullDelta, range := b.range }

Instances For

source

def Lapis.Server.SemanticTokens.OptionsBuilder.addTokenModifiers (b : OptionsBuilder) (modifiers : Array String) :

OptionsBuilder

Add custom token modifiers to the standard list

Equations

b.addTokenModifiers modifiers = { tokenTypes := b.tokenTypes, tokenModifiers := b.tokenModifiers ++ modifiers, full := b.full, fullDelta := b.fullDelta, range := b.range }