Language.LSP.Message.DocumentHighlight

Definitions

record DocumentHighlightClientCapabilities : Type

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

Totality: total
Visibility: public export
Constructor: 

MkDocumentHighlightClientCapabilities : Maybe Bool -> DocumentHighlightClientCapabilities

Projection: 

.dynamicRegistration : DocumentHighlightClientCapabilities -> Maybe Bool

Hints:

FromJSON DocumentHighlightClientCapabilities

ToJSON DocumentHighlightClientCapabilities

.dynamicRegistration : DocumentHighlightClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

dynamicRegistration : DocumentHighlightClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

record DocumentHighlightOptions : Type

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

Totality: total
Visibility: public export
Constructor: 

MkDocumentHighlightOptions : Maybe Bool -> DocumentHighlightOptions

Projection: 

.workDoneProgress : DocumentHighlightOptions -> Maybe Bool

Hints:

FromJSON DocumentHighlightOptions

ToJSON DocumentHighlightOptions

.workDoneProgress : DocumentHighlightOptions -> Maybe Bool

Totality: total
Visibility: public export

workDoneProgress : DocumentHighlightOptions -> Maybe Bool

Totality: total
Visibility: public export

record DocumentHighlightRegistrationOptions : Type

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

Totality: total
Visibility: public export
Constructor: 

MkDocumentHighlightRegistrationOptions : Maybe Bool -> OneOf [DocumentSelector, Null] -> DocumentHighlightRegistrationOptions

Projections:

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

.workDoneProgress : DocumentHighlightRegistrationOptions -> Maybe Bool

Hints:

FromJSON DocumentHighlightRegistrationOptions

ToJSON DocumentHighlightRegistrationOptions

.workDoneProgress : DocumentHighlightRegistrationOptions -> Maybe Bool

Totality: total
Visibility: public export

workDoneProgress : DocumentHighlightRegistrationOptions -> Maybe Bool

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

documentSelector : DocumentHighlightRegistrationOptions -> OneOf [DocumentSelector, Null]

Totality: total
Visibility: public export

record DocumentHighlightParams : Type

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

Totality: total
Visibility: public export
Constructor: 

MkDocumentHighlightParams : Maybe ProgressToken -> Maybe ProgressToken -> TextDocumentIdentifier -> Position -> DocumentHighlightParams

Projections:

.partialResultToken : DocumentHighlightParams -> Maybe ProgressToken

.position : DocumentHighlightParams -> Position

.textDocument : DocumentHighlightParams -> TextDocumentIdentifier

.workDoneToken : DocumentHighlightParams -> Maybe ProgressToken

Hints:

FromJSON DocumentHighlightParams

ToJSON DocumentHighlightParams

.workDoneToken : DocumentHighlightParams -> Maybe ProgressToken

Totality: total
Visibility: public export

workDoneToken : DocumentHighlightParams -> Maybe ProgressToken

Totality: total
Visibility: public export

.partialResultToken : DocumentHighlightParams -> Maybe ProgressToken

Totality: total
Visibility: public export

partialResultToken : DocumentHighlightParams -> Maybe ProgressToken

Totality: total
Visibility: public export

.textDocument : DocumentHighlightParams -> TextDocumentIdentifier

Totality: total
Visibility: public export

textDocument : DocumentHighlightParams -> TextDocumentIdentifier

Totality: total
Visibility: public export

.position : DocumentHighlightParams -> Position

Totality: total
Visibility: public export

position : DocumentHighlightParams -> Position

Totality: total
Visibility: public export

data DocumentHighlightKind : Type

Totality: total
Visibility: public export
Constructors:

Text : DocumentHighlightKind

Read : DocumentHighlightKind

Write : DocumentHighlightKind

Hints:

FromJSON DocumentHighlightKind

ToJSON DocumentHighlightKind

record DocumentHighlight : Type

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

Totality: total
Visibility: public export
Constructor: 

MkDocumentHighlight : Range -> Maybe DocumentHighlightKind -> DocumentHighlight

Projections:

.kind : DocumentHighlight -> Maybe DocumentHighlightKind

.range : DocumentHighlight -> Range

Hints:

FromJSON DocumentHighlight

ToJSON DocumentHighlight

.range : DocumentHighlight -> Range

Totality: total
Visibility: public export

range : DocumentHighlight -> Range

Totality: total
Visibility: public export

.kind : DocumentHighlight -> Maybe DocumentHighlightKind

Totality: total
Visibility: public export

kind : DocumentHighlight -> Maybe DocumentHighlightKind

Totality: total
Visibility: public export