Language.LSP.Message.Definition

Definitions

record DefinitionClientCapabilities : Type

  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_definition

Totality: total
Visibility: public export
Constructor: 

MkDefinitionClientCapabilities : Maybe Bool -> Maybe Bool -> DefinitionClientCapabilities

Projections:

.dynamicRegistration : DefinitionClientCapabilities -> Maybe Bool

.linkSupport : DefinitionClientCapabilities -> Maybe Bool

Hints:

FromJSON DefinitionClientCapabilities

ToJSON DefinitionClientCapabilities

.dynamicRegistration : DefinitionClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

dynamicRegistration : DefinitionClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

.linkSupport : DefinitionClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

linkSupport : DefinitionClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

record DefinitionOptions : Type

  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_definition

Totality: total
Visibility: public export
Constructor: 

MkDefinitionOptions : Maybe Bool -> DefinitionOptions

Projection: 

.workDoneProgress : DefinitionOptions -> Maybe Bool

Hints:

FromJSON DefinitionOptions

ToJSON DefinitionOptions

.workDoneProgress : DefinitionOptions -> Maybe Bool

Totality: total
Visibility: public export

workDoneProgress : DefinitionOptions -> Maybe Bool

Totality: total
Visibility: public export

record DefinitionRegistrationOptions : Type

  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_definition

Totality: total
Visibility: public export
Constructor: 

MkDefinitionRegistrationOptions : Maybe Bool -> OneOf [DocumentSelector, Null] -> DefinitionRegistrationOptions

Projections:

.documentSelector : DefinitionRegistrationOptions -> OneOf [DocumentSelector, Null]

.workDoneProgress : DefinitionRegistrationOptions -> Maybe Bool

Hints:

FromJSON DefinitionRegistrationOptions

ToJSON DefinitionRegistrationOptions

.workDoneProgress : DefinitionRegistrationOptions -> Maybe Bool

Totality: total
Visibility: public export

workDoneProgress : DefinitionRegistrationOptions -> Maybe Bool

Totality: total
Visibility: public export

.documentSelector : DefinitionRegistrationOptions -> OneOf [DocumentSelector, Null]

Totality: total
Visibility: public export

documentSelector : DefinitionRegistrationOptions -> OneOf [DocumentSelector, Null]

Totality: total
Visibility: public export

record DefinitionParams : Type

  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_definition

Totality: total
Visibility: public export
Constructor: 

MkDefinitionParams : Maybe ProgressToken -> Maybe ProgressToken -> TextDocumentIdentifier -> Position -> DefinitionParams

Projections:

.partialResultToken : DefinitionParams -> Maybe ProgressToken

.position : DefinitionParams -> Position

.textDocument : DefinitionParams -> TextDocumentIdentifier

.workDoneToken : DefinitionParams -> Maybe ProgressToken

Hints:

FromJSON DefinitionParams

ToJSON DefinitionParams

.workDoneToken : DefinitionParams -> Maybe ProgressToken

Totality: total
Visibility: public export

workDoneToken : DefinitionParams -> Maybe ProgressToken

Totality: total
Visibility: public export

.partialResultToken : DefinitionParams -> Maybe ProgressToken

Totality: total
Visibility: public export

partialResultToken : DefinitionParams -> Maybe ProgressToken

Totality: total
Visibility: public export

.textDocument : DefinitionParams -> TextDocumentIdentifier

Totality: total
Visibility: public export

textDocument : DefinitionParams -> TextDocumentIdentifier

Totality: total
Visibility: public export

.position : DefinitionParams -> Position

Totality: total
Visibility: public export

position : DefinitionParams -> Position

Totality: total
Visibility: public export

record TypeDefinitionClientCapabilities : Type

  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_typeDefinition

Totality: total
Visibility: public export
Constructor: 

MkTypeDefinitionClientCapabilities : Maybe Bool -> Maybe Bool -> TypeDefinitionClientCapabilities

Projections:

.dynamicRegistration : TypeDefinitionClientCapabilities -> Maybe Bool

.linkSupport : TypeDefinitionClientCapabilities -> Maybe Bool

Hints:

FromJSON TypeDefinitionClientCapabilities

ToJSON TypeDefinitionClientCapabilities

.dynamicRegistration : TypeDefinitionClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

dynamicRegistration : TypeDefinitionClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

.linkSupport : TypeDefinitionClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

linkSupport : TypeDefinitionClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

record TypeDefinitionOptions : Type

  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_typeDefinition

Totality: total
Visibility: public export
Constructor: 

MkTypeDefinitionOptions : Maybe Bool -> TypeDefinitionOptions

Projection: 

.workDoneProgress : TypeDefinitionOptions -> Maybe Bool

Hints:

FromJSON TypeDefinitionOptions

ToJSON TypeDefinitionOptions

.workDoneProgress : TypeDefinitionOptions -> Maybe Bool

Totality: total
Visibility: public export

workDoneProgress : TypeDefinitionOptions -> Maybe Bool

Totality: total
Visibility: public export

record TypeDefinitionRegistrationOptions : Type

  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_typeDefinition

Totality: total
Visibility: public export
Constructor: 

MkTypeDefinitionRegistrationOptions : Maybe Bool -> OneOf [DocumentSelector, Null] -> Maybe String -> TypeDefinitionRegistrationOptions

Projections:

.documentSelector : TypeDefinitionRegistrationOptions -> OneOf [DocumentSelector, Null]

.id : TypeDefinitionRegistrationOptions -> Maybe String

.workDoneProgress : TypeDefinitionRegistrationOptions -> Maybe Bool

Hints:

FromJSON TypeDefinitionRegistrationOptions

ToJSON TypeDefinitionRegistrationOptions

.workDoneProgress : TypeDefinitionRegistrationOptions -> Maybe Bool

Totality: total
Visibility: public export

workDoneProgress : TypeDefinitionRegistrationOptions -> Maybe Bool

Totality: total
Visibility: public export

.documentSelector : TypeDefinitionRegistrationOptions -> OneOf [DocumentSelector, Null]

Totality: total
Visibility: public export

documentSelector : TypeDefinitionRegistrationOptions -> OneOf [DocumentSelector, Null]

Totality: total
Visibility: public export

.id : TypeDefinitionRegistrationOptions -> Maybe String

Totality: total
Visibility: public export

id : TypeDefinitionRegistrationOptions -> Maybe String

Totality: total
Visibility: public export

record TypeDefinitionParams : Type

  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_typeDefinition

Totality: total
Visibility: public export
Constructor: 

MkTypeDefinitionParams : Maybe ProgressToken -> Maybe ProgressToken -> TextDocumentIdentifier -> Position -> TypeDefinitionParams

Projections:

.partialResultToken : TypeDefinitionParams -> Maybe ProgressToken

.position : TypeDefinitionParams -> Position

.textDocument : TypeDefinitionParams -> TextDocumentIdentifier

.workDoneToken : TypeDefinitionParams -> Maybe ProgressToken

Hints:

FromJSON TypeDefinitionParams

ToJSON TypeDefinitionParams

.workDoneToken : TypeDefinitionParams -> Maybe ProgressToken

Totality: total
Visibility: public export

workDoneToken : TypeDefinitionParams -> Maybe ProgressToken

Totality: total
Visibility: public export

.partialResultToken : TypeDefinitionParams -> Maybe ProgressToken

Totality: total
Visibility: public export

partialResultToken : TypeDefinitionParams -> Maybe ProgressToken

Totality: total
Visibility: public export

.textDocument : TypeDefinitionParams -> TextDocumentIdentifier

Totality: total
Visibility: public export

textDocument : TypeDefinitionParams -> TextDocumentIdentifier

Totality: total
Visibility: public export

.position : TypeDefinitionParams -> Position

Totality: total
Visibility: public export

position : TypeDefinitionParams -> Position

Totality: total
Visibility: public export