Idris2Doc : Language.LSP.Message.DocumentLink

Language.LSP.Message.DocumentLink

(source)

Definitions

record DocumentLinkClientCapabilities : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentLink

Totality: total
Visibility: public export
Constructor: 
MkDocumentLinkClientCapabilities : Maybe Bool -> Maybe Bool -> DocumentLinkClientCapabilities

Projections:
.dynamicRegistration : DocumentLinkClientCapabilities -> Maybe Bool
.tooltipSupport : DocumentLinkClientCapabilities -> Maybe Bool

Hints:
FromJSON DocumentLinkClientCapabilities
ToJSON DocumentLinkClientCapabilities
.dynamicRegistration : DocumentLinkClientCapabilities -> Maybe Bool
Totality: total
Visibility: public export
dynamicRegistration : DocumentLinkClientCapabilities -> Maybe Bool
Totality: total
Visibility: public export
.tooltipSupport : DocumentLinkClientCapabilities -> Maybe Bool
Totality: total
Visibility: public export
tooltipSupport : DocumentLinkClientCapabilities -> Maybe Bool
Totality: total
Visibility: public export
record DocumentLinkOptions : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentLink

Totality: total
Visibility: public export
Constructor: 
MkDocumentLinkOptions : Maybe Bool -> Maybe Bool -> DocumentLinkOptions

Projections:
.resolveProvider : DocumentLinkOptions -> Maybe Bool
.workDoneProgress : DocumentLinkOptions -> Maybe Bool

Hints:
FromJSON DocumentLinkOptions
ToJSON DocumentLinkOptions
.workDoneProgress : DocumentLinkOptions -> Maybe Bool
Totality: total
Visibility: public export
workDoneProgress : DocumentLinkOptions -> Maybe Bool
Totality: total
Visibility: public export
.resolveProvider : DocumentLinkOptions -> Maybe Bool
Totality: total
Visibility: public export
resolveProvider : DocumentLinkOptions -> Maybe Bool
Totality: total
Visibility: public export
record DocumentLinkRegistrationOptions : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentLink

Totality: total
Visibility: public export
Constructor: 
MkDocumentLinkRegistrationOptions : Maybe Bool -> Maybe Bool -> OneOf [DocumentSelector, Null] -> DocumentLinkRegistrationOptions

Projections:
.documentSelector : DocumentLinkRegistrationOptions -> OneOf [DocumentSelector, Null]
.resolveProvider : DocumentLinkRegistrationOptions -> Maybe Bool
.workDoneProgress : DocumentLinkRegistrationOptions -> Maybe Bool

Hints:
FromJSON DocumentLinkRegistrationOptions
ToJSON DocumentLinkRegistrationOptions
.workDoneProgress : DocumentLinkRegistrationOptions -> Maybe Bool
Totality: total
Visibility: public export
workDoneProgress : DocumentLinkRegistrationOptions -> Maybe Bool
Totality: total
Visibility: public export
.resolveProvider : DocumentLinkRegistrationOptions -> Maybe Bool
Totality: total
Visibility: public export
resolveProvider : DocumentLinkRegistrationOptions -> Maybe Bool
Totality: total
Visibility: public export
.documentSelector : DocumentLinkRegistrationOptions -> OneOf [DocumentSelector, Null]
Totality: total
Visibility: public export
documentSelector : DocumentLinkRegistrationOptions -> OneOf [DocumentSelector, Null]
Totality: total
Visibility: public export
record DocumentLinkParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentLink

Totality: total
Visibility: public export
Constructor: 
MkDocumentLinkParams : Maybe ProgressToken -> Maybe ProgressToken -> TextDocumentIdentifier -> DocumentLinkParams

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

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

Totality: total
Visibility: public export
Constructor: 

Projections:
.data_ : DocumentLink -> Maybe JSON
.range : DocumentLink -> Range
.target : DocumentLink -> Maybe DocumentURI
.tooltip : DocumentLink -> Maybe String

Hints:
FromJSON DocumentLink
ToJSON DocumentLink
.range : DocumentLink -> Range
Totality: total
Visibility: public export
range : DocumentLink -> Range
Totality: total
Visibility: public export
.target : DocumentLink -> Maybe DocumentURI
Totality: total
Visibility: public export
target : DocumentLink -> Maybe DocumentURI
Totality: total
Visibility: public export
.tooltip : DocumentLink -> Maybe String
Totality: total
Visibility: public export
tooltip : DocumentLink -> Maybe String
Totality: total
Visibility: public export
.data_ : DocumentLink -> Maybe JSON
Totality: total
Visibility: public export
data_ : DocumentLink -> Maybe JSON
Totality: total
Visibility: public export