Idris2Doc : Language.LSP.Message.CodeAction

Language.LSP.Message.CodeAction

(source)

Definitions

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

Totality: total
Visibility: public export
Constructors:
Empty : CodeActionKind
QuickFix : CodeActionKind
Refactor : CodeActionKind
RefactorExtract : CodeActionKind
RefactorInline : CodeActionKind
RefactorRewrite : CodeActionKind
Source : CodeActionKind
SourceOrganizeImport : CodeActionKind
Other : String->CodeActionKind

Hints:
EqCodeActionKind
FromJSONCodeActionKind
ToJSONCodeActionKind
recordCodeActionKindValueSet : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction

Totality: total
Visibility: public export
Constructor: 
MkCodeActionKindValueSet : ListCodeActionKind->CodeActionKindValueSet

Projection: 
.valueSet : CodeActionKindValueSet->ListCodeActionKind

Hints:
FromJSONCodeActionKindValueSet
ToJSONCodeActionKindValueSet
.valueSet : CodeActionKindValueSet->ListCodeActionKind
Totality: total
Visibility: public export
valueSet : CodeActionKindValueSet->ListCodeActionKind
Totality: total
Visibility: public export
recordCodeActionLiteralSupport : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction

Totality: total
Visibility: public export
Constructor: 
MkCodeActionLiteralSupport : CodeActionKindValueSet->CodeActionLiteralSupport

Projection: 
.codeActionKind : CodeActionLiteralSupport->CodeActionKindValueSet

Hints:
FromJSONCodeActionLiteralSupport
ToJSONCodeActionLiteralSupport
.codeActionKind : CodeActionLiteralSupport->CodeActionKindValueSet
Totality: total
Visibility: public export
codeActionKind : CodeActionLiteralSupport->CodeActionKindValueSet
Totality: total
Visibility: public export
recordResolveSupport : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction

Totality: total
Visibility: public export
Constructor: 
MkResolveSupport : ListString->ResolveSupport

Projection: 
.properties : ResolveSupport->ListString

Hints:
FromJSONResolveSupport
ToJSONResolveSupport
.properties : ResolveSupport->ListString
Totality: total
Visibility: public export
properties : ResolveSupport->ListString
Totality: total
Visibility: public export
recordCodeActionClientCapabilities : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction

Totality: total
Visibility: public export
Constructor: 
MkCodeActionClientCapabilities : MaybeBool->MaybeCodeActionLiteralSupport->MaybeBool->MaybeBool->MaybeBool->MaybeResolveSupport->MaybeBool->CodeActionClientCapabilities

Projections:
.codeActionLiteralSupport : CodeActionClientCapabilities->MaybeCodeActionLiteralSupport
.dataSupport : CodeActionClientCapabilities->MaybeBool
.disabledSupport : CodeActionClientCapabilities->MaybeBool
.dynamicRegistration : CodeActionClientCapabilities->MaybeBool
.honorsChangeAnnotations : CodeActionClientCapabilities->MaybeBool
.isPreferredSupport : CodeActionClientCapabilities->MaybeBool
.resolveSupport : CodeActionClientCapabilities->MaybeResolveSupport

Hints:
FromJSONCodeActionClientCapabilities
ToJSONCodeActionClientCapabilities
.dynamicRegistration : CodeActionClientCapabilities->MaybeBool
Totality: total
Visibility: public export
dynamicRegistration : CodeActionClientCapabilities->MaybeBool
Totality: total
Visibility: public export
.codeActionLiteralSupport : CodeActionClientCapabilities->MaybeCodeActionLiteralSupport
Totality: total
Visibility: public export
codeActionLiteralSupport : CodeActionClientCapabilities->MaybeCodeActionLiteralSupport
Totality: total
Visibility: public export
.isPreferredSupport : CodeActionClientCapabilities->MaybeBool
Totality: total
Visibility: public export
isPreferredSupport : CodeActionClientCapabilities->MaybeBool
Totality: total
Visibility: public export
.disabledSupport : CodeActionClientCapabilities->MaybeBool
Totality: total
Visibility: public export
disabledSupport : CodeActionClientCapabilities->MaybeBool
Totality: total
Visibility: public export
.dataSupport : CodeActionClientCapabilities->MaybeBool
Totality: total
Visibility: public export
dataSupport : CodeActionClientCapabilities->MaybeBool
Totality: total
Visibility: public export
.resolveSupport : CodeActionClientCapabilities->MaybeResolveSupport
Totality: total
Visibility: public export
resolveSupport : CodeActionClientCapabilities->MaybeResolveSupport
Totality: total
Visibility: public export
.honorsChangeAnnotations : CodeActionClientCapabilities->MaybeBool
Totality: total
Visibility: public export
honorsChangeAnnotations : CodeActionClientCapabilities->MaybeBool
Totality: total
Visibility: public export
recordCodeActionOptions : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction

Totality: total
Visibility: public export
Constructor: 
MkCodeActionOptions : MaybeBool->Maybe (ListCodeActionKind) ->MaybeBool->CodeActionOptions

Projections:
.codeActionKinds : CodeActionOptions->Maybe (ListCodeActionKind)
.resolveProvider : CodeActionOptions->MaybeBool
.workDoneProgress : CodeActionOptions->MaybeBool

Hints:
FromJSONCodeActionOptions
ToJSONCodeActionOptions
.workDoneProgress : CodeActionOptions->MaybeBool
Totality: total
Visibility: public export
workDoneProgress : CodeActionOptions->MaybeBool
Totality: total
Visibility: public export
.codeActionKinds : CodeActionOptions->Maybe (ListCodeActionKind)
Totality: total
Visibility: public export
codeActionKinds : CodeActionOptions->Maybe (ListCodeActionKind)
Totality: total
Visibility: public export
.resolveProvider : CodeActionOptions->MaybeBool
Totality: total
Visibility: public export
resolveProvider : CodeActionOptions->MaybeBool
Totality: total
Visibility: public export
recordCodeActionRegistrationOptions : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction

Totality: total
Visibility: public export
Constructor: 
MkCodeActionRegistrationOptions : MaybeBool->Maybe (ListCodeActionKind) ->MaybeBool->OneOf [DocumentSelector, Null] ->CodeActionRegistrationOptions

Projections:
.codeActionKinds : CodeActionRegistrationOptions->Maybe (ListCodeActionKind)
.documentSelector : CodeActionRegistrationOptions->OneOf [DocumentSelector, Null]
.resolveProvider : CodeActionRegistrationOptions->MaybeBool
.workDoneProgress : CodeActionRegistrationOptions->MaybeBool

Hints:
FromJSONCodeActionRegistrationOptions
ToJSONCodeActionRegistrationOptions
.workDoneProgress : CodeActionRegistrationOptions->MaybeBool
Totality: total
Visibility: public export
workDoneProgress : CodeActionRegistrationOptions->MaybeBool
Totality: total
Visibility: public export
.codeActionKinds : CodeActionRegistrationOptions->Maybe (ListCodeActionKind)
Totality: total
Visibility: public export
codeActionKinds : CodeActionRegistrationOptions->Maybe (ListCodeActionKind)
Totality: total
Visibility: public export
.resolveProvider : CodeActionRegistrationOptions->MaybeBool
Totality: total
Visibility: public export
resolveProvider : CodeActionRegistrationOptions->MaybeBool
Totality: total
Visibility: public export
.documentSelector : CodeActionRegistrationOptions->OneOf [DocumentSelector, Null]
Totality: total
Visibility: public export
documentSelector : CodeActionRegistrationOptions->OneOf [DocumentSelector, Null]
Totality: total
Visibility: public export
recordCodeActionContext : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction

Totality: total
Visibility: public export
Constructor: 
MkCodeActionContext : ListDiagnostic->Maybe (ListCodeActionKind) ->CodeActionContext

Projections:
.diagnostics : CodeActionContext->ListDiagnostic
.only : CodeActionContext->Maybe (ListCodeActionKind)

Hints:
FromJSONCodeActionContext
ToJSONCodeActionContext
.diagnostics : CodeActionContext->ListDiagnostic
Totality: total
Visibility: public export
diagnostics : CodeActionContext->ListDiagnostic
Totality: total
Visibility: public export
.only : CodeActionContext->Maybe (ListCodeActionKind)
Totality: total
Visibility: public export
only : CodeActionContext->Maybe (ListCodeActionKind)
Totality: total
Visibility: public export
recordCodeActionParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction

Totality: total
Visibility: public export
Constructor: 
MkCodeActionParams : MaybeProgressToken->MaybeProgressToken->TextDocumentIdentifier->Range->CodeActionContext->CodeActionParams

Projections:
.context : CodeActionParams->CodeActionContext
.partialResultToken : CodeActionParams->MaybeProgressToken
.range : CodeActionParams->Range
.textDocument : CodeActionParams->TextDocumentIdentifier
.workDoneToken : CodeActionParams->MaybeProgressToken

Hints:
FromJSONCodeActionParams
ToJSONCodeActionParams
.workDoneToken : CodeActionParams->MaybeProgressToken
Totality: total
Visibility: public export
workDoneToken : CodeActionParams->MaybeProgressToken
Totality: total
Visibility: public export
.partialResultToken : CodeActionParams->MaybeProgressToken
Totality: total
Visibility: public export
partialResultToken : CodeActionParams->MaybeProgressToken
Totality: total
Visibility: public export
.textDocument : CodeActionParams->TextDocumentIdentifier
Totality: total
Visibility: public export
textDocument : CodeActionParams->TextDocumentIdentifier
Totality: total
Visibility: public export
.range : CodeActionParams->Range
Totality: total
Visibility: public export
range : CodeActionParams->Range
Totality: total
Visibility: public export
.context : CodeActionParams->CodeActionContext
Totality: total
Visibility: public export
context : CodeActionParams->CodeActionContext
Totality: total
Visibility: public export
recordDisabled : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction

Totality: total
Visibility: public export
Constructor: 
MkDisabled : String->Disabled

Projection: 
.reason : Disabled->String

Hints:
FromJSONDisabled
ToJSONDisabled
.reason : Disabled->String
Totality: total
Visibility: public export
reason : Disabled->String
Totality: total
Visibility: public export
recordCodeAction : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction

Totality: total
Visibility: public export
Constructor: 
MkCodeAction : String->MaybeCodeActionKind->Maybe (ListDiagnostic) ->MaybeBool->MaybeDisabled->MaybeWorkspaceEdit->MaybeCommand->MaybeJSON->CodeAction

Projections:
.command : CodeAction->MaybeCommand
.data_ : CodeAction->MaybeJSON
.diagnostics : CodeAction->Maybe (ListDiagnostic)
.disabled : CodeAction->MaybeDisabled
.edit : CodeAction->MaybeWorkspaceEdit
.isPreferred : CodeAction->MaybeBool
.kind : CodeAction->MaybeCodeActionKind
.title : CodeAction->String

Hints:
FromJSONCodeAction
ToJSONCodeAction
.title : CodeAction->String
Totality: total
Visibility: public export
title : CodeAction->String
Totality: total
Visibility: public export
.kind : CodeAction->MaybeCodeActionKind
Totality: total
Visibility: public export
kind : CodeAction->MaybeCodeActionKind
Totality: total
Visibility: public export
.diagnostics : CodeAction->Maybe (ListDiagnostic)
Totality: total
Visibility: public export
diagnostics : CodeAction->Maybe (ListDiagnostic)
Totality: total
Visibility: public export
.isPreferred : CodeAction->MaybeBool
Totality: total
Visibility: public export
isPreferred : CodeAction->MaybeBool
Totality: total
Visibility: public export
.disabled : CodeAction->MaybeDisabled
Totality: total
Visibility: public export
disabled : CodeAction->MaybeDisabled
Totality: total
Visibility: public export
.edit : CodeAction->MaybeWorkspaceEdit
Totality: total
Visibility: public export
edit : CodeAction->MaybeWorkspaceEdit
Totality: total
Visibility: public export
.command : CodeAction->MaybeCommand
Totality: total
Visibility: public export
command : CodeAction->MaybeCommand
Totality: total
Visibility: public export
.data_ : CodeAction->MaybeJSON
Totality: total
Visibility: public export
data_ : CodeAction->MaybeJSON
Totality: total
Visibility: public export