Idris2Doc : Language.LSP.Message.SemanticTokens

Language.LSP.Message.SemanticTokens

(source)
Definitions
record SemanticTokenRequestsFull : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens

  Totality: total
  Visibility: public export
  Constructor: 
MkSemanticTokenRequestsFull : Maybe Bool -> SemanticTokenRequestsFull

  Projection: 
.delta : SemanticTokenRequestsFull -> Maybe Bool

  Hints:
  
FromJSON SemanticTokenRequestsFull
  
ToJSON SemanticTokenRequestsFull
.delta : SemanticTokenRequestsFull -> Maybe Bool
  Totality: total
  Visibility: public export
delta : SemanticTokenRequestsFull -> Maybe Bool
  Totality: total
  Visibility: public export
record SemanticTokenRequests : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens

  Totality: total
  Visibility: public export
  Constructor: 
MkSemanticTokenRequests : Maybe (OneOf [Bool, ()]) -> Maybe (OneOf [Bool, SemanticTokenRequestsFull]) -> SemanticTokenRequests

  Projections:
  
.full : SemanticTokenRequests -> Maybe (OneOf [Bool, SemanticTokenRequestsFull])
  
.range : SemanticTokenRequests -> Maybe (OneOf [Bool, ()])

  Hints:
  
FromJSON SemanticTokenRequests
  
ToJSON SemanticTokenRequests
.range : SemanticTokenRequests -> Maybe (OneOf [Bool, ()])
  Totality: total
  Visibility: public export
range : SemanticTokenRequests -> Maybe (OneOf [Bool, ()])
  Totality: total
  Visibility: public export
.full : SemanticTokenRequests -> Maybe (OneOf [Bool, SemanticTokenRequestsFull])
  Totality: total
  Visibility: public export
full : SemanticTokenRequests -> Maybe (OneOf [Bool, SemanticTokenRequestsFull])
  Totality: total
  Visibility: public export
data TokenFormat : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens

  Totality: total
  Visibility: public export
  Constructor: 
Relative : TokenFormat

  Hints:
  
FromJSON TokenFormat
  
ToJSON TokenFormat
record SemanticTokensLegend : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens

  Totality: total
  Visibility: public export
  Constructor: 
MkSemanticTokensLegend : List String -> List String -> SemanticTokensLegend

  Projections:
  
.tokenModifiers : SemanticTokensLegend -> List String
  
.tokenTypes : SemanticTokensLegend -> List String

  Hints:
  
FromJSON SemanticTokensLegend
  
ToJSON SemanticTokensLegend
.tokenTypes : SemanticTokensLegend -> List String
  Totality: total
  Visibility: public export
tokenTypes : SemanticTokensLegend -> List String
  Totality: total
  Visibility: public export
.tokenModifiers : SemanticTokensLegend -> List String
  Totality: total
  Visibility: public export
tokenModifiers : SemanticTokensLegend -> List String
  Totality: total
  Visibility: public export
record SemanticTokensClientCapabilities : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens

  Totality: total
  Visibility: public export
  Constructor: 
MkSemanticTokensClientCapabilities : Maybe Bool -> SemanticTokenRequests -> List String -> List String -> List TokenFormat -> Maybe Bool -> Maybe Bool -> SemanticTokensClientCapabilities

  Projections:
  
.dynamicRegistration : SemanticTokensClientCapabilities -> Maybe Bool
  
.formats : SemanticTokensClientCapabilities -> List TokenFormat
  
.multilineTokenSupport : SemanticTokensClientCapabilities -> Maybe Bool
  
.overlappingTokenSupport : SemanticTokensClientCapabilities -> Maybe Bool
  
.requests : SemanticTokensClientCapabilities -> SemanticTokenRequests
  
.tokenModifiers : SemanticTokensClientCapabilities -> List String
  
.tokenTypes : SemanticTokensClientCapabilities -> List String

  Hints:
  
FromJSON SemanticTokensClientCapabilities
  
ToJSON SemanticTokensClientCapabilities
.dynamicRegistration : SemanticTokensClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
dynamicRegistration : SemanticTokensClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
.requests : SemanticTokensClientCapabilities -> SemanticTokenRequests
  Totality: total
  Visibility: public export
requests : SemanticTokensClientCapabilities -> SemanticTokenRequests
  Totality: total
  Visibility: public export
.tokenTypes : SemanticTokensClientCapabilities -> List String
  Totality: total
  Visibility: public export
tokenTypes : SemanticTokensClientCapabilities -> List String
  Totality: total
  Visibility: public export
.tokenModifiers : SemanticTokensClientCapabilities -> List String
  Totality: total
  Visibility: public export
tokenModifiers : SemanticTokensClientCapabilities -> List String
  Totality: total
  Visibility: public export
.formats : SemanticTokensClientCapabilities -> List TokenFormat
  Totality: total
  Visibility: public export
formats : SemanticTokensClientCapabilities -> List TokenFormat
  Totality: total
  Visibility: public export
.overlappingTokenSupport : SemanticTokensClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
overlappingTokenSupport : SemanticTokensClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
.multilineTokenSupport : SemanticTokensClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
multilineTokenSupport : SemanticTokensClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
record SemanticTokensOptions : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens

  Totality: total
  Visibility: public export
  Constructor: 
MkSemanticTokensOptions : SemanticTokensLegend -> Maybe (OneOf [Bool, ()]) -> Maybe (OneOf [Bool, SemanticTokenRequestsFull]) -> SemanticTokensOptions

  Projections:
  
.full : SemanticTokensOptions -> Maybe (OneOf [Bool, SemanticTokenRequestsFull])
  
.legend : SemanticTokensOptions -> SemanticTokensLegend
  
.range : SemanticTokensOptions -> Maybe (OneOf [Bool, ()])

  Hints:
  
FromJSON SemanticTokensOptions
  
ToJSON SemanticTokensOptions
.legend : SemanticTokensOptions -> SemanticTokensLegend
  Totality: total
  Visibility: public export
legend : SemanticTokensOptions -> SemanticTokensLegend
  Totality: total
  Visibility: public export
.range : SemanticTokensOptions -> Maybe (OneOf [Bool, ()])
  Totality: total
  Visibility: public export
range : SemanticTokensOptions -> Maybe (OneOf [Bool, ()])
  Totality: total
  Visibility: public export
.full : SemanticTokensOptions -> Maybe (OneOf [Bool, SemanticTokenRequestsFull])
  Totality: total
  Visibility: public export
full : SemanticTokensOptions -> Maybe (OneOf [Bool, SemanticTokenRequestsFull])
  Totality: total
  Visibility: public export
record SemanticTokensRegistrationOptions : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens

  Totality: total
  Visibility: public export
  Constructor: 
MkSemanticTokensRegistrationOptions : SemanticTokensLegend -> Maybe (OneOf [Bool, ()]) -> Maybe (OneOf [Bool, SemanticTokenRequestsFull]) -> OneOf [DocumentSelector, Null] -> Maybe Bool -> SemanticTokensRegistrationOptions

  Projections:
  
.documentSelector : SemanticTokensRegistrationOptions -> OneOf [DocumentSelector, Null]
  
.full : SemanticTokensRegistrationOptions -> Maybe (OneOf [Bool, SemanticTokenRequestsFull])
  
.id : SemanticTokensRegistrationOptions -> Maybe Bool
  
.legend : SemanticTokensRegistrationOptions -> SemanticTokensLegend
  
.range : SemanticTokensRegistrationOptions -> Maybe (OneOf [Bool, ()])

  Hints:
  
FromJSON SemanticTokensRegistrationOptions
  
ToJSON SemanticTokensRegistrationOptions
.legend : SemanticTokensRegistrationOptions -> SemanticTokensLegend
  Totality: total
  Visibility: public export
legend : SemanticTokensRegistrationOptions -> SemanticTokensLegend
  Totality: total
  Visibility: public export
.range : SemanticTokensRegistrationOptions -> Maybe (OneOf [Bool, ()])
  Totality: total
  Visibility: public export
range : SemanticTokensRegistrationOptions -> Maybe (OneOf [Bool, ()])
  Totality: total
  Visibility: public export
.full : SemanticTokensRegistrationOptions -> Maybe (OneOf [Bool, SemanticTokenRequestsFull])
  Totality: total
  Visibility: public export
full : SemanticTokensRegistrationOptions -> Maybe (OneOf [Bool, SemanticTokenRequestsFull])
  Totality: total
  Visibility: public export
.documentSelector : SemanticTokensRegistrationOptions -> OneOf [DocumentSelector, Null]
  Totality: total
  Visibility: public export
documentSelector : SemanticTokensRegistrationOptions -> OneOf [DocumentSelector, Null]
  Totality: total
  Visibility: public export
.id : SemanticTokensRegistrationOptions -> Maybe Bool
  Totality: total
  Visibility: public export
id : SemanticTokensRegistrationOptions -> Maybe Bool
  Totality: total
  Visibility: public export
record SemanticTokensParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens

  Totality: total
  Visibility: public export
  Constructor: 
MkSemanticTokensParams : Maybe ProgressToken -> Maybe ProgressToken -> TextDocumentIdentifier -> SemanticTokensParams

  Projections:
  
.partialResultToken : SemanticTokensParams -> Maybe ProgressToken
  
.textDocument : SemanticTokensParams -> TextDocumentIdentifier
  
.workDoneToken : SemanticTokensParams -> Maybe ProgressToken

  Hints:
  
FromJSON SemanticTokensParams
  
ToJSON SemanticTokensParams
.workDoneToken : SemanticTokensParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
workDoneToken : SemanticTokensParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
.partialResultToken : SemanticTokensParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
partialResultToken : SemanticTokensParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
.textDocument : SemanticTokensParams -> TextDocumentIdentifier
  Totality: total
  Visibility: public export
textDocument : SemanticTokensParams -> TextDocumentIdentifier
  Totality: total
  Visibility: public export
record SemanticTokens : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens

  Totality: total
  Visibility: public export
  Constructor: 
MkSemanticTokens : Maybe String -> List Int -> SemanticTokens

  Projections:
  
.data_ : SemanticTokens -> List Int
  
.resultId : SemanticTokens -> Maybe String

  Hints:
  
FromJSON SemanticTokens
  
ToJSON SemanticTokens
.resultId : SemanticTokens -> Maybe String
  Totality: total
  Visibility: public export
resultId : SemanticTokens -> Maybe String
  Totality: total
  Visibility: public export
.data_ : SemanticTokens -> List Int
  Totality: total
  Visibility: public export
data_ : SemanticTokens -> List Int
  Totality: total
  Visibility: public export
record SemanticTokensPartialResult : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens

  Totality: total
  Visibility: public export
  Constructor: 
MkSemanticTokensPartialResult : List Int -> SemanticTokensPartialResult

  Projection: 
.data_ : SemanticTokensPartialResult -> List Int

  Hints:
  
FromJSON SemanticTokensPartialResult
  
ToJSON SemanticTokensPartialResult
.data_ : SemanticTokensPartialResult -> List Int
  Totality: total
  Visibility: public export
data_ : SemanticTokensPartialResult -> List Int
  Totality: total
  Visibility: public export
record SemanticTokensDeltaParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens

  Totality: total
  Visibility: public export
  Constructor: 
MkSemanticTokensDeltaParams : Maybe ProgressToken -> Maybe ProgressToken -> TextDocumentIdentifier -> String -> SemanticTokensDeltaParams

  Projections:
  
.partialResultToken : SemanticTokensDeltaParams -> Maybe ProgressToken
  
.previousResultId : SemanticTokensDeltaParams -> String
  
.textDocument : SemanticTokensDeltaParams -> TextDocumentIdentifier
  
.workDoneToken : SemanticTokensDeltaParams -> Maybe ProgressToken

  Hints:
  
FromJSON SemanticTokensDeltaParams
  
ToJSON SemanticTokensDeltaParams
.workDoneToken : SemanticTokensDeltaParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
workDoneToken : SemanticTokensDeltaParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
.partialResultToken : SemanticTokensDeltaParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
partialResultToken : SemanticTokensDeltaParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
.textDocument : SemanticTokensDeltaParams -> TextDocumentIdentifier
  Totality: total
  Visibility: public export
textDocument : SemanticTokensDeltaParams -> TextDocumentIdentifier
  Totality: total
  Visibility: public export
.previousResultId : SemanticTokensDeltaParams -> String
  Totality: total
  Visibility: public export
previousResultId : SemanticTokensDeltaParams -> String
  Totality: total
  Visibility: public export
record SemanticTokensEdit : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens

  Totality: total
  Visibility: public export
  Constructor: 
MkSemanticTokensEdit : Int -> Int -> Maybe (List Int) -> SemanticTokensEdit

  Projections:
  
.data_ : SemanticTokensEdit -> Maybe (List Int)
  
.deleteCount : SemanticTokensEdit -> Int
  
.start : SemanticTokensEdit -> Int

  Hints:
  
FromJSON SemanticTokensEdit
  
ToJSON SemanticTokensEdit
.start : SemanticTokensEdit -> Int
  Totality: total
  Visibility: public export
start : SemanticTokensEdit -> Int
  Totality: total
  Visibility: public export
.deleteCount : SemanticTokensEdit -> Int
  Totality: total
  Visibility: public export
deleteCount : SemanticTokensEdit -> Int
  Totality: total
  Visibility: public export
.data_ : SemanticTokensEdit -> Maybe (List Int)
  Totality: total
  Visibility: public export
data_ : SemanticTokensEdit -> Maybe (List Int)
  Totality: total
  Visibility: public export
record SemanticTokensDelta : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens

  Totality: total
  Visibility: public export
  Constructor: 
MkSemanticTokensDelta : Maybe String -> List SemanticTokensEdit -> SemanticTokensDelta

  Projections:
  
.edits : SemanticTokensDelta -> List SemanticTokensEdit
  
.resultId : SemanticTokensDelta -> Maybe String

  Hints:
  
FromJSON SemanticTokensDelta
  
ToJSON SemanticTokensDelta
.resultId : SemanticTokensDelta -> Maybe String
  Totality: total
  Visibility: public export
resultId : SemanticTokensDelta -> Maybe String
  Totality: total
  Visibility: public export
.edits : SemanticTokensDelta -> List SemanticTokensEdit
  Totality: total
  Visibility: public export
edits : SemanticTokensDelta -> List SemanticTokensEdit
  Totality: total
  Visibility: public export
record SemanticTokensDeltaPartialResult : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens

  Totality: total
  Visibility: public export
  Constructor: 
MkSemanticTokensDeltaPartialResult : List SemanticTokensEdit -> SemanticTokensDeltaPartialResult

  Projection: 
.edits : SemanticTokensDeltaPartialResult -> List SemanticTokensEdit

  Hints:
  
FromJSON SemanticTokensDeltaPartialResult
  
ToJSON SemanticTokensDeltaPartialResult
.edits : SemanticTokensDeltaPartialResult -> List SemanticTokensEdit
  Totality: total
  Visibility: public export
edits : SemanticTokensDeltaPartialResult -> List SemanticTokensEdit
  Totality: total
  Visibility: public export
record SemanticTokensRangeParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens

  Totality: total
  Visibility: public export
  Constructor: 
MkSemanticTokensRangeParams : Maybe ProgressToken -> Maybe ProgressToken -> TextDocumentIdentifier -> Range -> SemanticTokensRangeParams

  Projections:
  
.partialResultToken : SemanticTokensRangeParams -> Maybe ProgressToken
  
.range : SemanticTokensRangeParams -> Range
  
.textDocument : SemanticTokensRangeParams -> TextDocumentIdentifier
  
.workDoneToken : SemanticTokensRangeParams -> Maybe ProgressToken

  Hints:
  
FromJSON SemanticTokensRangeParams
  
ToJSON SemanticTokensRangeParams
.workDoneToken : SemanticTokensRangeParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
workDoneToken : SemanticTokensRangeParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
.partialResultToken : SemanticTokensRangeParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
partialResultToken : SemanticTokensRangeParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
.textDocument : SemanticTokensRangeParams -> TextDocumentIdentifier
  Totality: total
  Visibility: public export
textDocument : SemanticTokensRangeParams -> TextDocumentIdentifier
  Totality: total
  Visibility: public export
.range : SemanticTokensRangeParams -> Range
  Totality: total
  Visibility: public export
range : SemanticTokensRangeParams -> Range
  Totality: total
  Visibility: public export
record SemanticTokensWorkspaceClientCapabilities : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens

  Totality: total
  Visibility: public export
  Constructor: 
MkSemanticTokensWorkspaceClientCapabilities : Maybe Bool -> SemanticTokensWorkspaceClientCapabilities

  Projection: 
.refreshSupport : SemanticTokensWorkspaceClientCapabilities -> Maybe Bool

  Hints:
  
FromJSON SemanticTokensWorkspaceClientCapabilities
  
ToJSON SemanticTokensWorkspaceClientCapabilities
.refreshSupport : SemanticTokensWorkspaceClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
refreshSupport : SemanticTokensWorkspaceClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export