Idris2Doc : Language.LSP.Message.SelectionRange

Language.LSP.Message.SelectionRange

(source)

Definitions

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

Totality: total
Visibility: public export
Constructor: 
MkSelectionRangeClientCapabilities : Maybe Bool -> SelectionRangeClientCapabilities

Projection: 
.dynamicRegistration : SelectionRangeClientCapabilities -> Maybe Bool

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

Totality: total
Visibility: public export
Constructor: 
MkSelectionRangeOptions : Maybe Bool -> SelectionRangeOptions

Projection: 
.workDoneProgress : SelectionRangeOptions -> Maybe Bool

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

Totality: total
Visibility: public export
Constructor: 
MkSelectionRangeRegistrationOptions : Maybe Bool -> OneOf [DocumentSelector, Null] -> Maybe String -> SelectionRangeRegistrationOptions

Projections:
.documentSelector : SelectionRangeRegistrationOptions -> OneOf [DocumentSelector, Null]
.id : SelectionRangeRegistrationOptions -> Maybe String
.workDoneProgress : SelectionRangeRegistrationOptions -> Maybe Bool

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

Totality: total
Visibility: public export
Constructor: 
MkSelectionRangeParams : Maybe ProgressToken -> Maybe ProgressToken -> TextDocumentIdentifier -> List Position -> SelectionRangeParams

Projections:
.partialResultToken : SelectionRangeParams -> Maybe ProgressToken
.positions : SelectionRangeParams -> List Position
.textDocument : SelectionRangeParams -> TextDocumentIdentifier
.workDoneToken : SelectionRangeParams -> Maybe ProgressToken

Hints:
FromJSON SelectionRangeParams
ToJSON SelectionRangeParams
.workDoneToken : SelectionRangeParams -> Maybe ProgressToken
Totality: total
Visibility: public export
workDoneToken : SelectionRangeParams -> Maybe ProgressToken
Totality: total
Visibility: public export
.partialResultToken : SelectionRangeParams -> Maybe ProgressToken
Totality: total
Visibility: public export
partialResultToken : SelectionRangeParams -> Maybe ProgressToken
Totality: total
Visibility: public export
.textDocument : SelectionRangeParams -> TextDocumentIdentifier
Totality: total
Visibility: public export
textDocument : SelectionRangeParams -> TextDocumentIdentifier
Totality: total
Visibility: public export
.positions : SelectionRangeParams -> List Position
Totality: total
Visibility: public export
positions : SelectionRangeParams -> List Position
Totality: total
Visibility: public export
record SelectionRange : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_selectionRange

Totality: total
Visibility: public export
Constructor: 
MkSelectionRange : Range -> Maybe (Inf SelectionRange) -> SelectionRange

Projections:
.parent : SelectionRange -> Maybe (Inf SelectionRange)
.range : SelectionRange -> Range

Hints:
FromJSON SelectionRange
ToJSON SelectionRange
.range : SelectionRange -> Range
Totality: total
Visibility: public export
range : SelectionRange -> Range
Totality: total
Visibility: public export
.parent : SelectionRange -> Maybe (Inf SelectionRange)
Totality: total
Visibility: public export
parent : SelectionRange -> Maybe (Inf SelectionRange)
Totality: total
Visibility: public export