Language.LSP.Message.FoldingRange

Definitions

record FoldingRangeClientCapabilities : Type

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

Totality: total
Visibility: public export
Constructor: 

MkFoldingRangeClientCapabilities : Maybe Bool -> Maybe Int -> Maybe Bool -> FoldingRangeClientCapabilities

Projections:

.dynamicRegistration : FoldingRangeClientCapabilities -> Maybe Bool

.lineFoldingOnly : FoldingRangeClientCapabilities -> Maybe Bool

.rangeLimit : FoldingRangeClientCapabilities -> Maybe Int

Hints:

FromJSON FoldingRangeClientCapabilities

ToJSON FoldingRangeClientCapabilities

.dynamicRegistration : FoldingRangeClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

dynamicRegistration : FoldingRangeClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

.rangeLimit : FoldingRangeClientCapabilities -> Maybe Int

Totality: total
Visibility: public export

rangeLimit : FoldingRangeClientCapabilities -> Maybe Int

Totality: total
Visibility: public export

.lineFoldingOnly : FoldingRangeClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

lineFoldingOnly : FoldingRangeClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

record FoldingRangeOptions : Type

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

Totality: total
Visibility: public export
Constructor: 

MkFoldingRangeOptions : Maybe Bool -> FoldingRangeOptions

Projection: 

.workDoneProgress : FoldingRangeOptions -> Maybe Bool

Hints:

FromJSON FoldingRangeOptions

ToJSON FoldingRangeOptions

.workDoneProgress : FoldingRangeOptions -> Maybe Bool

Totality: total
Visibility: public export

workDoneProgress : FoldingRangeOptions -> Maybe Bool

Totality: total
Visibility: public export

record FoldingRangeRegistrationOptions : Type

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

Totality: total
Visibility: public export
Constructor: 

MkFoldingRangeRegistrationOptions : Maybe Bool -> OneOf [DocumentSelector, Null] -> Maybe String -> FoldingRangeRegistrationOptions

Projections:

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

.id : FoldingRangeRegistrationOptions -> Maybe String

.workDoneProgress : FoldingRangeRegistrationOptions -> Maybe Bool

Hints:

FromJSON FoldingRangeRegistrationOptions

ToJSON FoldingRangeRegistrationOptions

.workDoneProgress : FoldingRangeRegistrationOptions -> Maybe Bool

Totality: total
Visibility: public export

workDoneProgress : FoldingRangeRegistrationOptions -> Maybe Bool

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

documentSelector : FoldingRangeRegistrationOptions -> OneOf [DocumentSelector, Null]

Totality: total
Visibility: public export

.id : FoldingRangeRegistrationOptions -> Maybe String

Totality: total
Visibility: public export

id : FoldingRangeRegistrationOptions -> Maybe String

Totality: total
Visibility: public export

record FoldingRangeParams : Type

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

Totality: total
Visibility: public export
Constructor: 

MkFoldingRangeParams : Maybe ProgressToken -> Maybe ProgressToken -> TextDocumentIdentifier -> FoldingRangeParams

Projections:

.partialResultToken : FoldingRangeParams -> Maybe ProgressToken

.textDocument : FoldingRangeParams -> TextDocumentIdentifier

.workDoneToken : FoldingRangeParams -> Maybe ProgressToken

Hints:

FromJSON FoldingRangeParams

ToJSON FoldingRangeParams

.workDoneToken : FoldingRangeParams -> Maybe ProgressToken

Totality: total
Visibility: public export

workDoneToken : FoldingRangeParams -> Maybe ProgressToken

Totality: total
Visibility: public export

.partialResultToken : FoldingRangeParams -> Maybe ProgressToken

Totality: total
Visibility: public export

partialResultToken : FoldingRangeParams -> Maybe ProgressToken

Totality: total
Visibility: public export

.textDocument : FoldingRangeParams -> TextDocumentIdentifier

Totality: total
Visibility: public export

textDocument : FoldingRangeParams -> TextDocumentIdentifier

Totality: total
Visibility: public export

data FoldingRangeKind : Type

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

Totality: total
Visibility: public export
Constructors:

Comment : FoldingRangeKind

Imports : FoldingRangeKind

Region : FoldingRangeKind

Hints:

FromJSON FoldingRangeKind

ToJSON FoldingRangeKind

record FoldingRange : Type

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

Totality: total
Visibility: public export
Constructor: 

MkFoldingRange : Int -> Maybe Int -> Int -> Maybe Int -> Maybe String -> FoldingRange

Projections:

.endCharacter : FoldingRange -> Maybe Int

.endLine : FoldingRange -> Int

.kind : FoldingRange -> Maybe String

.startCharacter : FoldingRange -> Maybe Int

.startLine : FoldingRange -> Int

Hints:

FromJSON FoldingRange

ToJSON FoldingRange

.startLine : FoldingRange -> Int

Totality: total
Visibility: public export

startLine : FoldingRange -> Int

Totality: total
Visibility: public export

.startCharacter : FoldingRange -> Maybe Int

Totality: total
Visibility: public export

startCharacter : FoldingRange -> Maybe Int

Totality: total
Visibility: public export

.endLine : FoldingRange -> Int

Totality: total
Visibility: public export

endLine : FoldingRange -> Int

Totality: total
Visibility: public export

.endCharacter : FoldingRange -> Maybe Int

Totality: total
Visibility: public export

endCharacter : FoldingRange -> Maybe Int

Totality: total
Visibility: public export

.kind : FoldingRange -> Maybe String

Totality: total
Visibility: public export

kind : FoldingRange -> Maybe String

Totality: total
Visibility: public export