Language.LSP.Message.Hover

Definitions

record HoverClientCapabilities : Type

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

Totality: total
Visibility: public export
Constructor: 

MkHoverClientCapabilities : Maybe Bool -> Maybe (List MarkupKind) -> HoverClientCapabilities

Projections:

.contentFormat : HoverClientCapabilities -> Maybe (List MarkupKind)

.dynamicRegistration : HoverClientCapabilities -> Maybe Bool

Hints:

FromJSON HoverClientCapabilities

ToJSON HoverClientCapabilities

.dynamicRegistration : HoverClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

dynamicRegistration : HoverClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

.contentFormat : HoverClientCapabilities -> Maybe (List MarkupKind)

Totality: total
Visibility: public export

contentFormat : HoverClientCapabilities -> Maybe (List MarkupKind)

Totality: total
Visibility: public export

record HoverOptions : Type

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

Totality: total
Visibility: public export
Constructor: 

MkHoverOptions : Maybe Bool -> HoverOptions

Projection: 

.workDoneProgress : HoverOptions -> Maybe Bool

Hints:

FromJSON HoverOptions

ToJSON HoverOptions

.workDoneProgress : HoverOptions -> Maybe Bool

Totality: total
Visibility: public export

workDoneProgress : HoverOptions -> Maybe Bool

Totality: total
Visibility: public export

record HoverRegistrationOptions : Type

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

Totality: total
Visibility: public export
Constructor: 

MkHoverRegistrationOptions : Maybe Bool -> OneOf [DocumentSelector, Null] -> HoverRegistrationOptions

Projections:

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

.workDoneProgress : HoverRegistrationOptions -> Maybe Bool

Hints:

FromJSON HoverRegistrationOptions

ToJSON HoverRegistrationOptions

.workDoneProgress : HoverRegistrationOptions -> Maybe Bool

Totality: total
Visibility: public export

workDoneProgress : HoverRegistrationOptions -> Maybe Bool

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

documentSelector : HoverRegistrationOptions -> OneOf [DocumentSelector, Null]

Totality: total
Visibility: public export

record HoverParams : Type

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

Totality: total
Visibility: public export
Constructor: 

MkHoverParams : Maybe ProgressToken -> TextDocumentIdentifier -> Position -> HoverParams

Projections:

.position : HoverParams -> Position

.textDocument : HoverParams -> TextDocumentIdentifier

.workDoneToken : HoverParams -> Maybe ProgressToken

Hints:

FromJSON HoverParams

ToJSON HoverParams

.workDoneToken : HoverParams -> Maybe ProgressToken

Totality: total
Visibility: public export

workDoneToken : HoverParams -> Maybe ProgressToken

Totality: total
Visibility: public export

.textDocument : HoverParams -> TextDocumentIdentifier

Totality: total
Visibility: public export

textDocument : HoverParams -> TextDocumentIdentifier

Totality: total
Visibility: public export

.position : HoverParams -> Position

Totality: total
Visibility: public export

position : HoverParams -> Position

Totality: total
Visibility: public export

record Hover : Type

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

Totality: total
Visibility: public export
Constructor: 

MkHover : OneOf [MarkedString, List MarkedString, MarkupContent] -> Maybe Range -> Hover

Projections:

.contents : Hover -> OneOf [MarkedString, List MarkedString, MarkupContent]

.range : Hover -> Maybe Range

Hints:

FromJSON Hover

ToJSON Hover

.contents : Hover -> OneOf [MarkedString, List MarkedString, MarkupContent]

Totality: total
Visibility: public export

contents : Hover -> OneOf [MarkedString, List MarkedString, MarkupContent]

Totality: total
Visibility: public export

.range : Hover -> Maybe Range

Totality: total
Visibility: public export

range : Hover -> Maybe Range

Totality: total
Visibility: public export