Language.LSP.Message.Implementation

Definitions

record ImplementationClientCapabilities : Type

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

Totality: total
Visibility: public export
Constructor: 

MkImplementationClientCapabilities : Maybe Bool -> Maybe Bool -> ImplementationClientCapabilities

Projections:

.dynamicRegistration : ImplementationClientCapabilities -> Maybe Bool

.linkSupport : ImplementationClientCapabilities -> Maybe Bool

Hints:

FromJSON ImplementationClientCapabilities

ToJSON ImplementationClientCapabilities

.dynamicRegistration : ImplementationClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

dynamicRegistration : ImplementationClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

.linkSupport : ImplementationClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

linkSupport : ImplementationClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

record ImplementationOptions : Type

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

Totality: total
Visibility: public export
Constructor: 

MkImplementationOptions : Maybe Bool -> ImplementationOptions

Projection: 

.workDoneProgress : ImplementationOptions -> Maybe Bool

Hints:

FromJSON ImplementationOptions

ToJSON ImplementationOptions

.workDoneProgress : ImplementationOptions -> Maybe Bool

Totality: total
Visibility: public export

workDoneProgress : ImplementationOptions -> Maybe Bool

Totality: total
Visibility: public export

record ImplementationRegistrationOptions : Type

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

Totality: total
Visibility: public export
Constructor: 

MkImplementationRegistrationOptions : Maybe Bool -> OneOf [DocumentSelector, Null] -> Maybe String -> ImplementationRegistrationOptions

Projections:

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

.id : ImplementationRegistrationOptions -> Maybe String

.workDoneProgress : ImplementationRegistrationOptions -> Maybe Bool

Hints:

FromJSON ImplementationRegistrationOptions

ToJSON ImplementationRegistrationOptions

.workDoneProgress : ImplementationRegistrationOptions -> Maybe Bool

Totality: total
Visibility: public export

workDoneProgress : ImplementationRegistrationOptions -> Maybe Bool

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

documentSelector : ImplementationRegistrationOptions -> OneOf [DocumentSelector, Null]

Totality: total
Visibility: public export

.id : ImplementationRegistrationOptions -> Maybe String

Totality: total
Visibility: public export

id : ImplementationRegistrationOptions -> Maybe String

Totality: total
Visibility: public export

record ImplementationParams : Type

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

Totality: total
Visibility: public export
Constructor: 

MkImplementationParams : Maybe ProgressToken -> Maybe ProgressToken -> TextDocumentIdentifier -> Position -> ImplementationParams

Projections:

.partialResultToken : ImplementationParams -> Maybe ProgressToken

.position : ImplementationParams -> Position

.textDocument : ImplementationParams -> TextDocumentIdentifier

.workDoneToken : ImplementationParams -> Maybe ProgressToken

Hints:

FromJSON ImplementationParams

ToJSON ImplementationParams

.workDoneToken : ImplementationParams -> Maybe ProgressToken

Totality: total
Visibility: public export

workDoneToken : ImplementationParams -> Maybe ProgressToken

Totality: total
Visibility: public export

.partialResultToken : ImplementationParams -> Maybe ProgressToken

Totality: total
Visibility: public export

partialResultToken : ImplementationParams -> Maybe ProgressToken

Totality: total
Visibility: public export

.textDocument : ImplementationParams -> TextDocumentIdentifier

Totality: total
Visibility: public export

textDocument : ImplementationParams -> TextDocumentIdentifier

Totality: total
Visibility: public export

.position : ImplementationParams -> Position

Totality: total
Visibility: public export

position : ImplementationParams -> Position

Totality: total
Visibility: public export