Idris2Doc : Language.LSP.Message.Completion

Language.LSP.Message.Completion

(source)
Definitions
data CompletionItemKind : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion

  Totality: total
  Visibility: public export
  Constructors:
  
Text : CompletionItemKind
  
Method : CompletionItemKind
  
Function : CompletionItemKind
  
Constructor : CompletionItemKind
  
Field : CompletionItemKind
  
Variable : CompletionItemKind
  
Class : CompletionItemKind
  
Interface : CompletionItemKind
  
Module : CompletionItemKind
  
Property : CompletionItemKind
  
Unit_ : CompletionItemKind
  
Value : CompletionItemKind
  
Enum : CompletionItemKind
  
Keyword : CompletionItemKind
  
Snippet : CompletionItemKind
  
Color : CompletionItemKind
  
File : CompletionItemKind
  
Reference : CompletionItemKind
  
Folder : CompletionItemKind
  
EnumMember : CompletionItemKind
  
Constant : CompletionItemKind
  
Struct : CompletionItemKind
  
Event : CompletionItemKind
  
Operator : CompletionItemKind
  
TypeParameter : CompletionItemKind

  Hints:
  
FromJSON CompletionItemKind
  
ToJSON CompletionItemKind
data CompletionItemTag : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion

  Totality: total
  Visibility: public export
  Constructor: 
Deprecated : CompletionItemTag

  Hints:
  
FromJSON CompletionItemTag
  
ToJSON CompletionItemTag
data InsertTextMode : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion

  Totality: total
  Visibility: public export
  Constructors:
  
AsIs : InsertTextMode
  
AdjustIndentation : InsertTextMode

  Hints:
  
FromJSON InsertTextMode
  
ToJSON InsertTextMode
data InsertTextFormat : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion

  Totality: total
  Visibility: public export
  Constructors:
  
PlainText : InsertTextFormat
  
Snippet : InsertTextFormat

  Hints:
  
FromJSON InsertTextFormat
  
ToJSON InsertTextFormat
record CompletionItemTagSupportClientCapabilities : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion

  Totality: total
  Visibility: public export
  Constructor: 
MkCompletionItemTagSupportClientCapabilities : List CompletionItemTag -> CompletionItemTagSupportClientCapabilities

  Projection: 
.valueSet : CompletionItemTagSupportClientCapabilities -> List CompletionItemTag

  Hints:
  
FromJSON CompletionItemTagSupportClientCapabilities
  
ToJSON CompletionItemTagSupportClientCapabilities
.valueSet : CompletionItemTagSupportClientCapabilities -> List CompletionItemTag
  Totality: total
  Visibility: public export
valueSet : CompletionItemTagSupportClientCapabilities -> List CompletionItemTag
  Totality: total
  Visibility: public export
record CompletionItemResolveSupportClientCapabilities : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion

  Totality: total
  Visibility: public export
  Constructor: 
MkCompletionItemResolveSupportClientCapabilities : List String -> CompletionItemResolveSupportClientCapabilities

  Projection: 
.properties : CompletionItemResolveSupportClientCapabilities -> List String

  Hints:
  
FromJSON CompletionItemResolveSupportClientCapabilities
  
ToJSON CompletionItemResolveSupportClientCapabilities
.properties : CompletionItemResolveSupportClientCapabilities -> List String
  Totality: total
  Visibility: public export
properties : CompletionItemResolveSupportClientCapabilities -> List String
  Totality: total
  Visibility: public export
record InsertTextModeSupport : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion

  Totality: total
  Visibility: public export
  Constructor: 
MkInsertTextModeSupport : List InsertTextMode -> InsertTextModeSupport

  Projection: 
.valueSet : InsertTextModeSupport -> List InsertTextMode

  Hints:
  
FromJSON InsertTextModeSupport
  
ToJSON InsertTextModeSupport
.valueSet : InsertTextModeSupport -> List InsertTextMode
  Totality: total
  Visibility: public export
valueSet : InsertTextModeSupport -> List InsertTextMode
  Totality: total
  Visibility: public export
record CompletionItemClientCapabilities : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion

  Totality: total
  Visibility: public export
  Constructor: 
MkCompletionItemClientCapabilities : Maybe Bool -> Maybe Bool -> Maybe (List MarkupKind) -> Maybe Bool -> Maybe Bool -> Maybe CompletionItemTagSupportClientCapabilities -> Maybe Bool -> Maybe CompletionItemResolveSupportClientCapabilities -> Maybe InsertTextModeSupport -> CompletionItemClientCapabilities

  Projections:
  
.commitCharactersSupport : CompletionItemClientCapabilities -> Maybe Bool
  
.deprecatedSupport : CompletionItemClientCapabilities -> Maybe Bool
  
.documentationFormat : CompletionItemClientCapabilities -> Maybe (List MarkupKind)
  
.insertReplaceSupport : CompletionItemClientCapabilities -> Maybe Bool
  
.insertTextModeSupport : CompletionItemClientCapabilities -> Maybe InsertTextModeSupport
  
.preselectSupport : CompletionItemClientCapabilities -> Maybe Bool
  
.resolveSupport : CompletionItemClientCapabilities -> Maybe CompletionItemResolveSupportClientCapabilities
  
.snippetSupport : CompletionItemClientCapabilities -> Maybe Bool
  
.tagSupport : CompletionItemClientCapabilities -> Maybe CompletionItemTagSupportClientCapabilities

  Hints:
  
FromJSON CompletionItemClientCapabilities
  
ToJSON CompletionItemClientCapabilities
.snippetSupport : CompletionItemClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
snippetSupport : CompletionItemClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
.commitCharactersSupport : CompletionItemClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
commitCharactersSupport : CompletionItemClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
.documentationFormat : CompletionItemClientCapabilities -> Maybe (List MarkupKind)
  Totality: total
  Visibility: public export
documentationFormat : CompletionItemClientCapabilities -> Maybe (List MarkupKind)
  Totality: total
  Visibility: public export
.deprecatedSupport : CompletionItemClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
deprecatedSupport : CompletionItemClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
.preselectSupport : CompletionItemClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
preselectSupport : CompletionItemClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
.tagSupport : CompletionItemClientCapabilities -> Maybe CompletionItemTagSupportClientCapabilities
  Totality: total
  Visibility: public export
tagSupport : CompletionItemClientCapabilities -> Maybe CompletionItemTagSupportClientCapabilities
  Totality: total
  Visibility: public export
.insertReplaceSupport : CompletionItemClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
insertReplaceSupport : CompletionItemClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
.resolveSupport : CompletionItemClientCapabilities -> Maybe CompletionItemResolveSupportClientCapabilities
  Totality: total
  Visibility: public export
resolveSupport : CompletionItemClientCapabilities -> Maybe CompletionItemResolveSupportClientCapabilities
  Totality: total
  Visibility: public export
.insertTextModeSupport : CompletionItemClientCapabilities -> Maybe InsertTextModeSupport
  Totality: total
  Visibility: public export
insertTextModeSupport : CompletionItemClientCapabilities -> Maybe InsertTextModeSupport
  Totality: total
  Visibility: public export
record CompletionItemKindClientCapabilities : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion

  Totality: total
  Visibility: public export
  Constructor: 
MkCompletionItemKindClientCapabilities : Maybe (List CompletionItemKind) -> CompletionItemKindClientCapabilities

  Projection: 
.valueSet : CompletionItemKindClientCapabilities -> Maybe (List CompletionItemKind)

  Hints:
  
FromJSON CompletionItemKindClientCapabilities
  
ToJSON CompletionItemKindClientCapabilities
.valueSet : CompletionItemKindClientCapabilities -> Maybe (List CompletionItemKind)
  Totality: total
  Visibility: public export
valueSet : CompletionItemKindClientCapabilities -> Maybe (List CompletionItemKind)
  Totality: total
  Visibility: public export
record CompletionClientCapabilities : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion

  Totality: total
  Visibility: public export
  Constructor: 
MkCompletionClientCapabilities : Maybe Bool -> Maybe CompletionItemClientCapabilities -> Maybe CompletionItemKindClientCapabilities -> Maybe Bool -> CompletionClientCapabilities

  Projections:
  
.completionItem : CompletionClientCapabilities -> Maybe CompletionItemClientCapabilities
  
.completionItemKind : CompletionClientCapabilities -> Maybe CompletionItemKindClientCapabilities
  
.contextSupport : CompletionClientCapabilities -> Maybe Bool
  
.dynamicRegistration : CompletionClientCapabilities -> Maybe Bool

  Hints:
  
FromJSON CompletionClientCapabilities
  
ToJSON CompletionClientCapabilities
.dynamicRegistration : CompletionClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
dynamicRegistration : CompletionClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
.completionItem : CompletionClientCapabilities -> Maybe CompletionItemClientCapabilities
  Totality: total
  Visibility: public export
completionItem : CompletionClientCapabilities -> Maybe CompletionItemClientCapabilities
  Totality: total
  Visibility: public export
.completionItemKind : CompletionClientCapabilities -> Maybe CompletionItemKindClientCapabilities
  Totality: total
  Visibility: public export
completionItemKind : CompletionClientCapabilities -> Maybe CompletionItemKindClientCapabilities
  Totality: total
  Visibility: public export
.contextSupport : CompletionClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
contextSupport : CompletionClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
record CompletionOptions : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion

  Totality: total
  Visibility: public export
  Constructor: 
MkCompletionOptions : Maybe Bool -> Maybe (List Char) -> Maybe (List Char) -> Maybe Bool -> CompletionOptions

  Projections:
  
.allCommitCharacters : CompletionOptions -> Maybe (List Char)
  
.resolveProvider : CompletionOptions -> Maybe Bool
  
.triggerCharacters : CompletionOptions -> Maybe (List Char)
  
.workDoneProgress : CompletionOptions -> Maybe Bool

  Hints:
  
FromJSON CompletionOptions
  
ToJSON CompletionOptions
.workDoneProgress : CompletionOptions -> Maybe Bool
  Totality: total
  Visibility: public export
workDoneProgress : CompletionOptions -> Maybe Bool
  Totality: total
  Visibility: public export
.triggerCharacters : CompletionOptions -> Maybe (List Char)
  Totality: total
  Visibility: public export
triggerCharacters : CompletionOptions -> Maybe (List Char)
  Totality: total
  Visibility: public export
.allCommitCharacters : CompletionOptions -> Maybe (List Char)
  Totality: total
  Visibility: public export
allCommitCharacters : CompletionOptions -> Maybe (List Char)
  Totality: total
  Visibility: public export
.resolveProvider : CompletionOptions -> Maybe Bool
  Totality: total
  Visibility: public export
resolveProvider : CompletionOptions -> Maybe Bool
  Totality: total
  Visibility: public export
record CompletionRegistrationOptions : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion

  Totality: total
  Visibility: public export
  Constructor: 
MkCompletionRegistrationOptions : OneOf [DocumentSelector, Null] -> Maybe Bool -> Maybe (List Char) -> Maybe (List Char) -> Maybe Bool -> CompletionRegistrationOptions

  Projections:
  
.allCommitCharacters : CompletionRegistrationOptions -> Maybe (List Char)
  
.documentSelector : CompletionRegistrationOptions -> OneOf [DocumentSelector, Null]
  
.resolveProvider : CompletionRegistrationOptions -> Maybe Bool
  
.triggerCharacters : CompletionRegistrationOptions -> Maybe (List Char)
  
.workDoneProgress : CompletionRegistrationOptions -> Maybe Bool

  Hints:
  
FromJSON CompletionRegistrationOptions
  
ToJSON CompletionRegistrationOptions
.documentSelector : CompletionRegistrationOptions -> OneOf [DocumentSelector, Null]
  Totality: total
  Visibility: public export
documentSelector : CompletionRegistrationOptions -> OneOf [DocumentSelector, Null]
  Totality: total
  Visibility: public export
.workDoneProgress : CompletionRegistrationOptions -> Maybe Bool
  Totality: total
  Visibility: public export
workDoneProgress : CompletionRegistrationOptions -> Maybe Bool
  Totality: total
  Visibility: public export
.triggerCharacters : CompletionRegistrationOptions -> Maybe (List Char)
  Totality: total
  Visibility: public export
triggerCharacters : CompletionRegistrationOptions -> Maybe (List Char)
  Totality: total
  Visibility: public export
.allCommitCharacters : CompletionRegistrationOptions -> Maybe (List Char)
  Totality: total
  Visibility: public export
allCommitCharacters : CompletionRegistrationOptions -> Maybe (List Char)
  Totality: total
  Visibility: public export
.resolveProvider : CompletionRegistrationOptions -> Maybe Bool
  Totality: total
  Visibility: public export
resolveProvider : CompletionRegistrationOptions -> Maybe Bool
  Totality: total
  Visibility: public export
data CompletionTriggerKind : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion

  Totality: total
  Visibility: public export
  Constructors:
  
Invoked : CompletionTriggerKind
  
TriggerCharacter : CompletionTriggerKind
  
TriggerForIncompleteCompletions : CompletionTriggerKind

  Hints:
  
FromJSON CompletionTriggerKind
  
ToJSON CompletionTriggerKind
record CompletionContext : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion

  Totality: total
  Visibility: public export
  Constructor: 
MkCompletionContext : CompletionTriggerKind -> Maybe String -> CompletionContext

  Projections:
  
.triggerCharacter : CompletionContext -> Maybe String
  
.triggerKind : CompletionContext -> CompletionTriggerKind

  Hints:
  
FromJSON CompletionContext
  
ToJSON CompletionContext
.triggerKind : CompletionContext -> CompletionTriggerKind
  Totality: total
  Visibility: public export
triggerKind : CompletionContext -> CompletionTriggerKind
  Totality: total
  Visibility: public export
.triggerCharacter : CompletionContext -> Maybe String
  Totality: total
  Visibility: public export
triggerCharacter : CompletionContext -> Maybe String
  Totality: total
  Visibility: public export
record CompletionParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion

  Totality: total
  Visibility: public export
  Constructor: 
MkCompletionParams : TextDocumentIdentifier -> Position -> Maybe ProgressToken -> Maybe ProgressToken -> Maybe CompletionContext -> CompletionParams

  Projections:
  
.context : CompletionParams -> Maybe CompletionContext
  
.partialResultToken : CompletionParams -> Maybe ProgressToken
  
.position : CompletionParams -> Position
  
.textDocument : CompletionParams -> TextDocumentIdentifier
  
.workDoneToken : CompletionParams -> Maybe ProgressToken

  Hints:
  
FromJSON CompletionParams
  
ToJSON CompletionParams
.textDocument : CompletionParams -> TextDocumentIdentifier
  Totality: total
  Visibility: public export
textDocument : CompletionParams -> TextDocumentIdentifier
  Totality: total
  Visibility: public export
.position : CompletionParams -> Position
  Totality: total
  Visibility: public export
position : CompletionParams -> Position
  Totality: total
  Visibility: public export
.workDoneToken : CompletionParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
workDoneToken : CompletionParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
.partialResultToken : CompletionParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
partialResultToken : CompletionParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
.context : CompletionParams -> Maybe CompletionContext
  Totality: total
  Visibility: public export
context : CompletionParams -> Maybe CompletionContext
  Totality: total
  Visibility: public export
record CompletionItem : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion

  Totality: total
  Visibility: public export
  Constructor: 
MkCompletionItem : String -> Maybe CompletionItemKind -> Maybe (List CompletionItemTag) -> Maybe String -> Maybe (OneOf [String, MarkupContent]) -> Maybe Bool -> Maybe Bool -> Maybe String -> Maybe String -> Maybe String -> Maybe InsertTextFormat -> Maybe InsertTextMode -> Maybe (OneOf [TextEdit, InsertReplaceEdit]) -> Maybe (List TextEdit) -> Maybe (List Char) -> Maybe Command -> Maybe JSON -> CompletionItem

  Projections:
  
.additionalTextEdits : CompletionItem -> Maybe (List TextEdit)
  
.command : CompletionItem -> Maybe Command
  
.commitCharacters : CompletionItem -> Maybe (List Char)
  
.data_ : CompletionItem -> Maybe JSON
  
.deprecated : CompletionItem -> Maybe Bool
  
.detail : CompletionItem -> Maybe String
  
.documentation : CompletionItem -> Maybe (OneOf [String, MarkupContent])
  
.filterText : CompletionItem -> Maybe String
  
.insertText : CompletionItem -> Maybe String
  
.insertTextFormat : CompletionItem -> Maybe InsertTextFormat
  
.insertTextMode : CompletionItem -> Maybe InsertTextMode
  
.kind : CompletionItem -> Maybe CompletionItemKind
  
.label : CompletionItem -> String
  
.preselect : CompletionItem -> Maybe Bool
  
.sortText : CompletionItem -> Maybe String
  
.tags : CompletionItem -> Maybe (List CompletionItemTag)
  
.textEdit : CompletionItem -> Maybe (OneOf [TextEdit, InsertReplaceEdit])

  Hints:
  
FromJSON CompletionItem
  
ToJSON CompletionItem
.label : CompletionItem -> String
  Totality: total
  Visibility: public export
label : CompletionItem -> String
  Totality: total
  Visibility: public export
.kind : CompletionItem -> Maybe CompletionItemKind
  Totality: total
  Visibility: public export
kind : CompletionItem -> Maybe CompletionItemKind
  Totality: total
  Visibility: public export
.tags : CompletionItem -> Maybe (List CompletionItemTag)
  Totality: total
  Visibility: public export
tags : CompletionItem -> Maybe (List CompletionItemTag)
  Totality: total
  Visibility: public export
.detail : CompletionItem -> Maybe String
  Totality: total
  Visibility: public export
detail : CompletionItem -> Maybe String
  Totality: total
  Visibility: public export
.documentation : CompletionItem -> Maybe (OneOf [String, MarkupContent])
  Totality: total
  Visibility: public export
documentation : CompletionItem -> Maybe (OneOf [String, MarkupContent])
  Totality: total
  Visibility: public export
.deprecated : CompletionItem -> Maybe Bool
  Totality: total
  Visibility: public export
deprecated : CompletionItem -> Maybe Bool
  Totality: total
  Visibility: public export
.preselect : CompletionItem -> Maybe Bool
  Totality: total
  Visibility: public export
preselect : CompletionItem -> Maybe Bool
  Totality: total
  Visibility: public export
.sortText : CompletionItem -> Maybe String
  Totality: total
  Visibility: public export
sortText : CompletionItem -> Maybe String
  Totality: total
  Visibility: public export
.filterText : CompletionItem -> Maybe String
  Totality: total
  Visibility: public export
filterText : CompletionItem -> Maybe String
  Totality: total
  Visibility: public export
.insertText : CompletionItem -> Maybe String
  Totality: total
  Visibility: public export
insertText : CompletionItem -> Maybe String
  Totality: total
  Visibility: public export
.insertTextFormat : CompletionItem -> Maybe InsertTextFormat
  Totality: total
  Visibility: public export
insertTextFormat : CompletionItem -> Maybe InsertTextFormat
  Totality: total
  Visibility: public export
.insertTextMode : CompletionItem -> Maybe InsertTextMode
  Totality: total
  Visibility: public export
insertTextMode : CompletionItem -> Maybe InsertTextMode
  Totality: total
  Visibility: public export
.textEdit : CompletionItem -> Maybe (OneOf [TextEdit, InsertReplaceEdit])
  Totality: total
  Visibility: public export
textEdit : CompletionItem -> Maybe (OneOf [TextEdit, InsertReplaceEdit])
  Totality: total
  Visibility: public export
.additionalTextEdits : CompletionItem -> Maybe (List TextEdit)
  Totality: total
  Visibility: public export
additionalTextEdits : CompletionItem -> Maybe (List TextEdit)
  Totality: total
  Visibility: public export
.commitCharacters : CompletionItem -> Maybe (List Char)
  Totality: total
  Visibility: public export
commitCharacters : CompletionItem -> Maybe (List Char)
  Totality: total
  Visibility: public export
.command : CompletionItem -> Maybe Command
  Totality: total
  Visibility: public export
command : CompletionItem -> Maybe Command
  Totality: total
  Visibility: public export
.data_ : CompletionItem -> Maybe JSON
  Totality: total
  Visibility: public export
data_ : CompletionItem -> Maybe JSON
  Totality: total
  Visibility: public export
record CompletionList : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion

  Totality: total
  Visibility: public export
  Constructor: 
MkCompletionList : Bool -> List CompletionItem -> CompletionList

  Projections:
  
.isIncomplete : CompletionList -> Bool
  
.items : CompletionList -> List CompletionItem

  Hints:
  
FromJSON CompletionList
  
ToJSON CompletionList
.isIncomplete : CompletionList -> Bool
  Totality: total
  Visibility: public export
isIncomplete : CompletionList -> Bool
  Totality: total
  Visibility: public export
.items : CompletionList -> List CompletionItem
  Totality: total
  Visibility: public export
items : CompletionList -> List CompletionItem
  Totality: total
  Visibility: public export