Idris2Doc : Language.LSP.Message.CodeLens

Language.LSP.Message.CodeLens

(source)
Definitions
record CodeLensClientCapabilities : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeLens

  Totality: total
  Visibility: public export
  Constructor: 
MkCodeLensClientCapabilities : Maybe Bool -> CodeLensClientCapabilities

  Projection: 
.dynamicRegistration : CodeLensClientCapabilities -> Maybe Bool

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

  Totality: total
  Visibility: public export
  Constructor: 
MkCodeLensOptions : Maybe Bool -> Maybe Bool -> CodeLensOptions

  Projections:
  
.resolveProvider : CodeLensOptions -> Maybe Bool
  
.workDoneProgress : CodeLensOptions -> Maybe Bool

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

  Totality: total
  Visibility: public export
  Constructor: 
MkCodeLensRegistrationOptions : Maybe Bool -> Maybe Bool -> OneOf [DocumentSelector, Null] -> CodeLensRegistrationOptions

  Projections:
  
.documentSelector : CodeLensRegistrationOptions -> OneOf [DocumentSelector, Null]
  
.resolveProvider : CodeLensRegistrationOptions -> Maybe Bool
  
.workDoneProgress : CodeLensRegistrationOptions -> Maybe Bool

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

  Totality: total
  Visibility: public export
  Constructor: 
MkCodeLensParams : Maybe ProgressToken -> Maybe ProgressToken -> TextDocumentIdentifier -> CodeLensParams

  Projections:
  
.partialResultToken : CodeLensParams -> Maybe ProgressToken
  
.textDocument : CodeLensParams -> TextDocumentIdentifier
  
.workDoneToken : CodeLensParams -> Maybe ProgressToken

  Hints:
  
FromJSON CodeLensParams
  
ToJSON CodeLensParams
.workDoneToken : CodeLensParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
workDoneToken : CodeLensParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
.partialResultToken : CodeLensParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
partialResultToken : CodeLensParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
.textDocument : CodeLensParams -> TextDocumentIdentifier
  Totality: total
  Visibility: public export
textDocument : CodeLensParams -> TextDocumentIdentifier
  Totality: total
  Visibility: public export
record CodeLens : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeLens

  Totality: total
  Visibility: public export
  Constructor: 
MkCodeLens : Range -> Maybe Command -> Maybe JSON -> CodeLens

  Projections:
  
.command : CodeLens -> Maybe Command
  
.data_ : CodeLens -> Maybe JSON
  
.range : CodeLens -> Range

  Hints:
  
FromJSON CodeLens
  
ToJSON CodeLens
.range : CodeLens -> Range
  Totality: total
  Visibility: public export
range : CodeLens -> Range
  Totality: total
  Visibility: public export
.command : CodeLens -> Maybe Command
  Totality: total
  Visibility: public export
command : CodeLens -> Maybe Command
  Totality: total
  Visibility: public export
.data_ : CodeLens -> Maybe JSON
  Totality: total
  Visibility: public export
data_ : CodeLens -> Maybe JSON
  Totality: total
  Visibility: public export
record CodeLensWorkspaceClientCapabilities : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#codeLens_refresh

  Totality: total
  Visibility: public export
  Constructor: 
MkCodeLensWorkspaceClientCapabilities : Maybe Bool -> CodeLensWorkspaceClientCapabilities

  Projection: 
.refreshSupport : CodeLensWorkspaceClientCapabilities -> Maybe Bool

  Hints:
  
FromJSON CodeLensWorkspaceClientCapabilities
  
ToJSON CodeLensWorkspaceClientCapabilities
.refreshSupport : CodeLensWorkspaceClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
refreshSupport : CodeLensWorkspaceClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export