Language.LSP.Message.Rename

Definitions

data PrepareSupportDefaultBehaviour : Type

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

Totality: total
Visibility: public export
Constructor: 

Identifier : PrepareSupportDefaultBehaviour

Hints:

FromJSON PrepareSupportDefaultBehaviour

ToJSON PrepareSupportDefaultBehaviour

record RenameClientCapabilities : Type

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

Totality: total
Visibility: public export
Constructor: 

MkRenameClientCapabilities : Maybe Bool -> Maybe Bool -> Maybe PrepareSupportDefaultBehaviour -> Maybe Bool -> RenameClientCapabilities

Projections:

.dynamicRegistration : RenameClientCapabilities -> Maybe Bool

.honorsChangeAnnotation : RenameClientCapabilities -> Maybe Bool

.prepareSupport : RenameClientCapabilities -> Maybe Bool

.prepareSupportDefaultBehaviour : RenameClientCapabilities -> Maybe PrepareSupportDefaultBehaviour

Hints:

FromJSON RenameClientCapabilities

ToJSON RenameClientCapabilities

.dynamicRegistration : RenameClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

dynamicRegistration : RenameClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

.prepareSupport : RenameClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

prepareSupport : RenameClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

.prepareSupportDefaultBehaviour : RenameClientCapabilities -> Maybe PrepareSupportDefaultBehaviour

Totality: total
Visibility: public export

prepareSupportDefaultBehaviour : RenameClientCapabilities -> Maybe PrepareSupportDefaultBehaviour

Totality: total
Visibility: public export

.honorsChangeAnnotation : RenameClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

honorsChangeAnnotation : RenameClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

record RenameOptions : Type

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

Totality: total
Visibility: public export
Constructor: 

MkRenameOptions : Maybe Bool -> Maybe Bool -> RenameOptions

Projections:

.prepareProvider : RenameOptions -> Maybe Bool

.workDoneProgress : RenameOptions -> Maybe Bool

Hints:

FromJSON RenameOptions

ToJSON RenameOptions

.workDoneProgress : RenameOptions -> Maybe Bool

Totality: total
Visibility: public export

workDoneProgress : RenameOptions -> Maybe Bool

Totality: total
Visibility: public export

.prepareProvider : RenameOptions -> Maybe Bool

Totality: total
Visibility: public export

prepareProvider : RenameOptions -> Maybe Bool

Totality: total
Visibility: public export

record RenameRegistrationOptions : Type

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

Totality: total
Visibility: public export
Constructor: 

MkRenameRegistrationOptions : Maybe Bool -> Maybe Bool -> OneOf [DocumentSelector, Null] -> RenameRegistrationOptions

Projections:

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

.prepareProvider : RenameRegistrationOptions -> Maybe Bool

.workDoneProgress : RenameRegistrationOptions -> Maybe Bool

Hints:

FromJSON RenameRegistrationOptions

ToJSON RenameRegistrationOptions

.workDoneProgress : RenameRegistrationOptions -> Maybe Bool

Totality: total
Visibility: public export

workDoneProgress : RenameRegistrationOptions -> Maybe Bool

Totality: total
Visibility: public export

.prepareProvider : RenameRegistrationOptions -> Maybe Bool

Totality: total
Visibility: public export

prepareProvider : RenameRegistrationOptions -> Maybe Bool

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

documentSelector : RenameRegistrationOptions -> OneOf [DocumentSelector, Null]

Totality: total
Visibility: public export

record RenameParams : Type

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

Totality: total
Visibility: public export
Constructor: 

MkRenameParams : Maybe ProgressToken -> TextDocumentIdentifier -> String -> RenameParams

Projections:

.newName : RenameParams -> String

.textDocument : RenameParams -> TextDocumentIdentifier

.workDoneToken : RenameParams -> Maybe ProgressToken

Hints:

FromJSON RenameParams

ToJSON RenameParams

.workDoneToken : RenameParams -> Maybe ProgressToken

Totality: total
Visibility: public export

workDoneToken : RenameParams -> Maybe ProgressToken

Totality: total
Visibility: public export

.textDocument : RenameParams -> TextDocumentIdentifier

Totality: total
Visibility: public export

textDocument : RenameParams -> TextDocumentIdentifier

Totality: total
Visibility: public export

.newName : RenameParams -> String

Totality: total
Visibility: public export

newName : RenameParams -> String

Totality: total
Visibility: public export

record PrepareRenameParams : Type

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

Totality: total
Visibility: public export
Constructor: 

MkPrepareRenameParams : TextDocumentIdentifier -> Position -> PrepareRenameParams

Projections:

.position : PrepareRenameParams -> Position

.textDocument : PrepareRenameParams -> TextDocumentIdentifier

Hints:

FromJSON PrepareRenameParams

ToJSON PrepareRenameParams

.textDocument : PrepareRenameParams -> TextDocumentIdentifier

Totality: total
Visibility: public export

textDocument : PrepareRenameParams -> TextDocumentIdentifier

Totality: total
Visibility: public export

.position : PrepareRenameParams -> Position

Totality: total
Visibility: public export

position : PrepareRenameParams -> Position

Totality: total
Visibility: public export

record PrepareRenameDefaultResponse : Type

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

Totality: total
Visibility: public export
Constructor: 

MkPrepareRenameDefaultResponse : Bool -> PrepareRenameDefaultResponse

Projection: 

.defaultBehaviour : PrepareRenameDefaultResponse -> Bool

Hints:

FromJSON PrepareRenameDefaultResponse

ToJSON PrepareRenameDefaultResponse

.defaultBehaviour : PrepareRenameDefaultResponse -> Bool

Totality: total
Visibility: public export

defaultBehaviour : PrepareRenameDefaultResponse -> Bool

Totality: total
Visibility: public export

record PrepareRenamePlaceholderResponse : Type

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

Totality: total
Visibility: public export
Constructor: 

MkPrepareRenamePlaceholderResponse : Range -> String -> PrepareRenamePlaceholderResponse

Projections:

.placeholder : PrepareRenamePlaceholderResponse -> String

.range : PrepareRenamePlaceholderResponse -> Range

Hints:

FromJSON PrepareRenamePlaceholderResponse

ToJSON PrepareRenamePlaceholderResponse

.range : PrepareRenamePlaceholderResponse -> Range

Totality: total
Visibility: public export

range : PrepareRenamePlaceholderResponse -> Range

Totality: total
Visibility: public export

.placeholder : PrepareRenamePlaceholderResponse -> String

Totality: total
Visibility: public export

placeholder : PrepareRenamePlaceholderResponse -> String

Totality: total
Visibility: public export